This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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), |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open BinNums | |
open Datatypes | |
open Mat | |
open Nat | |
open Path | |
type coq_Node = | |
| A | |
| B | |
| C |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open BinNums | |
open Datatypes | |
open Mat | |
open Nat | |
open Path | |
type coq_Node = | |
| A | |
| B | |
| C |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. | |
Declare Scope regex_scope. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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 := |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** | |
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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! |
NewerOlder