mukeshtiwari

From Stdlib Require Import Utf8.


Section Equality.

  (* https://xavierleroy.org/CdF/2018-2019/10.pdf *)
  Definition Leibniz_eq {A : Type} (x y : A) : Prop :=
    ∀ (P : A -> Prop), P x <-> P y.
    
  Theorem Leibniz_equality_forward {A : Type} : 

mukeshtiwari

Section T. 
  
  Variables (A : Type) (B : A -> Type).

  Inductive W : Type := suc : forall (a : A), (B a -> W) -> W.

  Variables (P : W -> Type).
  Fixpoint rec (H : forall a f, (forall b, P (f b)) -> P (suc a f)) (x : W) : P x
    := match x with suc a f => H a f (fun b => rec H (f b)) end.

mukeshtiwari

From Stdlib Require Import 
  Vector Fin Bool Utf8
  Psatz BinIntDef.
Import VectorNotations EqNotations. 


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

mukeshtiwari

From Stdlib Require Import Utf8 Fin Psatz List.

Definition cardinality (n : nat) (A : Type) : Prop :=
  exists (f : A -> Fin.t n) (g : Fin.t n -> A),
    (forall x, g (f x) = x) ∧ (forall y, f (g y) = y).


Definition bool_to_Fin_2 (x : bool) : Fin.t 2 :=
  if x then Fin.FS Fin.F1 else Fin.F1.

mukeshtiwari

From Stdlib Require Import Utf8 Fin Psatz.

Definition cardinality (n : nat) (A : Type) : Prop :=
  exists (f : A -> Fin.t n) (g : Fin.t n -> A),
    (forall x, g (f x) = x) ∧ (forall y, f (g y) = y).


Definition bool_to_Fin_2 (x : bool) : Fin.t 2 :=
  if x then Fin.FS Fin.F1 else Fin.F1.

mukeshtiwari

Section Listmat.

  Context {Node R : Type} 
  (dec_node : forall (c d : Node), {c = d} + {c <> d}).


  Fixpoint cross_product (la lb : list Node) : 
    (list (Node * Node)) :=
    match la with 

mukeshtiwari

import qualified Prelude

__ :: any
__ = Prelude.error "Logical or arity value used"

data Bool =
   True
 | False
 deriving (Prelude.Show)

mukeshtiwari

From Stdlib Require Import Utf8 Vector Fin Psatz.
Import VectorNotations.

Section UIP.

  (* Set Printing Implicit. *)
  Theorem uip_nat : ∀ (n : nat) (pf : n = n), pf = @eq_refl nat n.
  Proof.
    refine(fix fn (n : nat) : ∀ (pf : n = n), pf = @eq_refl nat n := 
      match n as n' in nat return 

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.