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 :=

mukeshtiwari

Section Gcd. 

  Fixpoint gcd_rec (a b : nat) (acc : Acc lt b) {struct acc} : nat :=
    match Nat.eq_dec b 0 with 
    | left _ => a 
    | right Ha => gcd_rec b (Nat.modulo a b) 
      (Acc_inv acc (Nat.mod_upper_bound a b Ha))
    end.
    
  Definition gcd (a b : nat) : nat.