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.

mukeshtiwari

From Coq Require Import 
Relation_Operators Utf8 Psatz Wf_nat.


Section Morp.

  Variable A : Type.
  Variable B : Type.
  Variable leA : A -> A -> Prop. (* A relation on type A *)
  Variable leB : B -> B -> Prop. (* A relation on type B *)

mukeshtiwari

From Coq Require Import 
Relation_Operators Utf8 Psatz Wf_nat.


Section Jason. 

  Context {A B : Type}
  (f : A * B -> nat).

  Theorem fn_acc : forall (n : nat) (au : A) (bu : B),

mukeshtiwari

open BinNums
open Datatypes
open Mat
open Nat
open Path

type coq_Node =
| A
| B
| C

mukeshtiwari

open BinNums
open Datatypes
open Mat
open Nat
open Path

type coq_Node =
| A
| B
| C

mukeshtiwari

section cantor

  /-
    Mapping from natural numbers to integers is injective.
    We map even numbers to positive integers and odd numbers to negative integers.
    0 => 0
    1 => -1
    2 => 1

mukeshtiwari

(* Is this definition correct? *)
  Definition ltR (u v : R) : bool :=
  match u, v with 
  | Left x, Left y => Nat.ltb x y 
  | Left x, Infinity => true 
  | Infinity, Left _ => false 
  | _, _ => false
  end.

  Definition plusR (u v : R) : R :=