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
Inductive day : Type := | |
| monday : day | |
| tuesday : day | |
| wednesday : day | |
| thursday : day | |
| friday : day | |
| saturday : day | |
| sunday :day. | |
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 Export Lists_J. | |
Inductive boollist : Type := | |
|bool_nil : boollist | |
|bool_cons : bool -> boollist -> boollist. | |
Inductive list (X:Type) : Type := | |
|nil:list X | |
|cons : X -> list X -> list X. |
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 Export Poly_J. | |
Print double. | |
Theorem double_injective_FAILED: | |
forall n m, double n = double m -> n = m. | |
Proof. | |
intros n m. | |
induction n as [| n']. | |
Case "n=0". simpl. intros eq. |
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 Export Poly_J. | |
Check (2+2=4). | |
Check (ble_nat 3 2 = false). | |
Check 2+2. | |
Check ble_nat. | |
Check ble_nat 3 2. | |
Check false. | |
Check (2+2=5). |
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
(* | |
exercise palindromes | |
日本語:http://proofcafe.org/sf/Prop_J.html#lab200 | |
英語:https://www.cis.upenn.edu/~bcpierce/sf/current/Prop.html#lab266 | |
*) | |
(* 多相的なリストのInductive *) | |
Inductive list (X:Type) : Type := | |
| nil : list X | |
| cons : X -> list X -> list X. |
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
(* | |
exercise rev_injective | |
日本語:http://proofcafe.org/sf/Lists_J.html#lab63 | |
英語:https://www.cis.upenn.edu/~bcpierce/sf/current/Lists.html#lab89 | |
*) | |
(* 自然数のリストのInductive *) | |
Inductive natlist : Type := | |
| nil : natlist | |
| cons : nat -> natlist -> natlist. |
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
(* | |
式とは,シンボルや記号をつなげたもの | |
Eval simpl inで確認する | |
*) | |
Eval simpl in (1). | |
Eval simpl in (2). | |
Eval simpl in (nat). | |
Eval simpl in (Set). | |
Eval simpl in (1=2). |
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
(* 巨大数 *) | |
Print nat. | |
Definition 十 := 10. | |
Fixpoint plus (n m:nat) : nat := | |
match n with | |
| O => m | |
| S n' => S (plus n' m) |
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
Inductive bool : Type := |true | false. | |
Inductive eq A x : A -> Prop := eq_refl : eq A x x. | |
Inductive or A B : Prop:= | |
| or_introl : A -> or A B | |
| or_intror : B -> or A B. | |
Definition case_bool x : or (eq bool x true) (eq bool x false) := | |
match x with |
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
Variable A:Set. | |
Inductive Vec : nat -> Set:= | |
| VNil : Vec 0 | |
| VCons : forall n, A -> Vec n -> Vec (S n). | |
Print Vec. | |
Inductive bool := | true | false. |
OlderNewer