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) -> 

mukeshtiwari

The Different Types of Equality

I don't have much to say about this topic since I don't fully understand it.

Basically here are the types of equality I've found:

• Axiomatic
• Defined
• Identity

mukeshtiwari

(* In relation to https://cstheory.stackexchange.com/questions/40631/how-can-you-build-a-coinductive-memoization-table-for-recursive-functions-over-b *)
Require Import Vectors.Vector.
Import VectorNotations.

Set Primitive Projections.
Set Implicit Arguments.

Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -> binTree -> binTree.