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.

mukeshtiwari

(base) mukesh.tiwari@Mukeshs-MacBook-Pro-2 ~ % opam upgrade
The following actions will be performed:
=== recompile 9 packages
  ↻ coq-elpi                2.2.3              [uses elpi, ppx_optcomp]
  ↻ lsp                     1.18.0             [uses ppx_yojson_conv_lib]
  ↻ ocaml-lsp-server        1.18.0~5.2preview  [uses base, ppx_yojson_conv_lib]
  ↻ ocamlformat             0.26.2             [uses ocamlformat-lib]
  ↻ ocamlformat-lib         0.26.2             [uses base, stdio]
  ↻ ppx_deriving            6.0.2              [uses ppxlib]
  ↻ ppx_import              1.11.0             [uses ppxlib]

mukeshtiwari

CoInductive coAcc {A : Type} (R : A -> A -> Prop) (x : A) : Prop :=
| coAcc_intro : (forall y : A, R x y -> coAcc R y) -> coAcc R x. 


CoFixpoint coacc_rect :
  forall (A : Type) (R : A -> A -> Prop) (P : A -> Type), 
  (forall x : A, (forall y : A, R x y -> coAcc R y) -> 
  (forall y : A, R x y -> P y) -> P x) -> forall x : A, coAcc R x -> P x :=
  fun (A : Type) (R : A -> A -> Prop) (P : A -> Type)
  (f : (forall x : A, (forall y : A, R x y -> coAcc R y) ->