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.

mukeshtiwari

(**
Skip to [Definition decode_aux] to see the main definition.
*)

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.

mukeshtiwari

mukeshtiwari@Mukeshs-MacBook-Pro exercises % make
coq_makefile -f _CoqProject -o Makefile.coq
/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq
COQDEP VFILES
*** Warning: in file MetaCoqPrelude.v, library All is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file MetaCoqPrelude.v, library Checker is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file MetaCoqPrelude.v, library Reduction is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library All is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library Checker is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library Reduction is required from root MetaCoq.Template and has not been found in the loadpath!

mukeshtiwari

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.

Require Import Lia.
Require Import Relation_Definitions.