blob: 6250794526de06a9bd6bef389ea33f77c7118daf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
Require Export Coq.subtac.SubtacTactics.
Set Implicit Arguments.
Notation "'fun' { x : A | P } => Q" :=
(fun x:{x:A|P} => Q)
(at level 200, x ident, right associativity).
Notation " {{ x }} " := (tt : { y : unit | x }).
Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
Notation " ! " := (False_rect _ _).
Require Import Coq.Bool.Sumbool.
Notation "'dec'" := (sumbool_of_bool) (at level 0).
Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
intros.
induction t.
exact x.
Defined.
Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P),
P (ex_pi1 t).
intros A P.
dependent inversion t.
simpl.
exact p.
Defined.
Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
Notation "'forall' { x : A | P } , Q" :=
(forall x:{x:A|P}, Q)
(at level 200, x ident, right associativity).
Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
(t : sig P), P (` t).
Proof.
intros.
induction t.
simpl ; auto.
Qed.
Lemma equal_f : forall A B : Type, forall (f g : A -> B),
f = g -> forall x, f x = g x.
Proof.
intros.
rewrite H.
auto.
Qed.
Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ;
try (solve [ red ; intros ; discriminate ]) ; auto with arith.
Extraction Inline proj1_sig.
Extract Inductive unit => "unit" [ "()" ].
Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
Axiom pair : Type -> Type -> Type.
Extract Constant pair "'a" "'b" => " 'a * 'b ".
Extract Inductive prod => "pair" [ "" ].
Extract Inductive sigT => "pair" [ "" ].
Require Export ProofIrrelevance.
Delimit Scope program_scope with program.
|
