mukeshtiwari

Require Import Fin Utf8.

Notation "'Sigma' x .. y , p" :=
  (sig (fun x => .. (sig (fun y => p)) ..))
    (at level 200, x binder, right associativity,
     format "'[' 'Sigma'  '/  ' x  ..  y ,  '/  ' p ']'")
  : type_scope.


Theorem fin_inv : ∀ (n : nat) (f : Fin.t n), 

mukeshtiwari

From Coq Require Import List Utf8 Bool.


Section Propositional.

  Inductive Formula : Type :=
  | atom : nat -> Formula
  | imp : Formula -> Formula -> Formula
  | bot : Formula. 

mukeshtiwari

Section Gcd.

  Fixpoint gcd_rec (n m : nat) (acc : Acc lt (n + m)) {struct acc} :  nat.
  Proof.
    refine
        (match n as n' return n = n' -> _
         with
         | 0 => fun Ha  => m
         | S n' =>

mukeshtiwari

open Wikimedia


let string_candidates : coq_Node -> string = function
| TC   (* Ting Chen (Wing) *) -> "Ting Chen (Wing)"
| SK   (* Samuel Klein (Sj) *) -> "Samuel Klein (Sj)"
| KW   (* Kat Walsh (mindspillage) *) -> "Kat Walsh (mindspillage)"
| MR   (* Milos Rancic (Millosh) *) -> "Milos Rancic (Millosh)"
| LG   (* Lodewijk Gelauff (Effeietsanders) *) -> "Lodewijk Gelauff (Effeietsanders)"
| CB   (* Claudi Balaguer (Capsot) *) -> "Claudi Balaguer (Capsot)"

mukeshtiwari

open Mat
open Nat
open Path

type coq_Node =
| TC
| SK
| KW
| MR
| LG

mukeshtiwari

open Definitions
open List
open Path

(** val get_row : ('a1, 'a2) coq_Matrix -> 'a1 -> 'a1 -> 'a2 **)

let get_row m =
  m

(** val get_col : ('a1, 'a2) coq_Matrix -> 'a1 -> 'a1 -> 'a2 **)

mukeshtiwari

function encode (plain : nat, key : nat) : (out : nat)
  requires 0 <= plain < 26
  requires 0 <= key < 26
  ensures 0 <= out < 26
  ensures (plain + key >= 26) ==> out == plain + key - 26
  ensures plain + key < 26 ==> out == plain + key
{
  if plain + key >= 26 then
    plain + key - 26 
  else

mukeshtiwari

From Coq Require Import
  Program.Tactics
  List Psatz.


Definition nth_safe {A : Type}
  (l : list A) (n : nat) (Ha : (n < length l)) : A.
Proof.
  refine
    (match (nth_error l n) as nth return (nth_error l n) = nth -> A with

mukeshtiwari

Require Import Lia
  Coq.Bool.Bool
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith
  Coq.Lists.List.

Open Scope N_scope.

mukeshtiwari

From Coq Require Import
  Program.Tactics
  List Psatz.


Program Definition nth_safe {A} (l: list A) (n: nat) (IN: (n < length l)%nat) : A :=
  match (nth_error l n) with
    | Some res => res
    | None => _
  end.