-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathOverture.v
125 lines (94 loc) · 4.56 KB
/
Overture.v
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
(* -*- coq-prog-args: ("-top" "TTLT.MLTT2.Overture") -*- *)
Require Export TLTT.MyTacs.
Global Set Warnings "-notation-overridden".
Notation idmap := (fun x => x).
Notation compose := (fun g f x => g (f x)).
Notation " g 'o' f " := (compose g f) (at level 40, left associativity) : core_scope.
Set Primitive Projections.
Record sigT {A} (P : A -> Type) := exist { π1 : A ; π2 : P π1 }.
Arguments exist {_} _ _ _.
Scheme sigT_rect := Induction for sigT Sort Type.
Notation "{ x & P }" := (sigT (fun x => P)) (only parsing) : type_scope.
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) (only parsing) : type_scope.
Notation "'exists' x .. y , P"
:= (sigT (fun x => .. (sigT (fun y => P)) ..))
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "∃ x .. y , P"
:= (sigT (fun x => .. (sigT (fun y => P)) ..))
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "( x ; y )" := (exist _ x y) : core_scope.
Notation "( x ; y ; z )" := (x ; (y ; z)) : core_scope.
(* Notation "( x ; y ; .. ; z )" := (exist _ .. (exist _ x y) .. z) : core_scope. *)
Notation pr1 := (π1 _).
Notation pr2 := (π2 _).
Notation "x .1" := (π1 _ x) (at level 3, format "x '.1'") : core_scope.
Notation "x .2" := (π2 _ x) (at level 3, format "x '.2'") : core_scope.
Definition prod A B := sigT (fun _ : A => B).
Notation "A * B" := (prod A B) (at level 40, left associativity) : type_scope.
Notation "A × B" := (prod A B) (at level 90, right associativity) : type_scope.
Definition pair {A B} : A -> B -> A × B := fun x y => (x; y).
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Definition fst {A B} : A × B -> A := pr1.
Definition snd {A B} : A × B -> B := pr2.
Definition iff (A B : Type) := (A -> B) × (B -> A).
Notation "A <-> B" := (iff A B)%type : type_scope.
Definition transitive_iff {A B C}
: A <-> B -> B <-> C -> A <-> C.
Proof.
intros H1 H2. split; firstorder.
Defined.
Open Scope type_scope.
(* ********* Strict Eq ********* *)
Declare Scope eq_scope.
Delimit Scope eq_scope with eq.
Open Scope eq_scope.
(* Local Unset Elimination Schemes. *)
(* Inductive Eq {A: Type} (a: A) : A -> Type := *)
(* refl : Eq a a. *)
(* Arguments refl {A a} , [A] a. *)
(* Scheme Eq_ind := Induction for Eq Sort Type. *)
(* Arguments Eq_ind [A] a P f y e. *)
(* Scheme Eq_rec := Minimality for Eq Sort Type. *)
(* Arguments Eq_rec [A] a P f y e. *)
Definition Eq {A : Type} := eq (A:=A).
Definition refl {A : Type}(x : A) := eq_refl (A :=A) x.
Notation "x ≡ y :> A"
:= (@Eq A x y) (at level 70, y at next level, no associativity) : type_scope.
Notation "x ≡ y"
:= (@Eq _ x y) (at level 70, no associativity) : type_scope.
Axiom Eq_UIP : forall {A: Type} {x y: A} (p q: x ≡ y), p ≡ q.
Axiom Eq_proof_irrel : forall {P : Prop} (p q : P), p ≡ q.
Lemma Eq_rew A a y P (X : P a) (H : a ≡ y :> A) : P y.
Proof. rewrite <- H. assumption. Defined.
Lemma Eq_rew_r A a y P (X : P y) (H : a ≡ y :> A) : P a.
Proof. rewrite H. assumption. Defined.
Bind Scope eq_scope with Eq.
Definition Einverse {A : Type} {x y : A} (p : x ≡ y) : y ≡ x.
symmetry; assumption.
Defined.
Arguments Einverse {A x y} p : simpl nomatch.
Definition Econcat {A : Type} {x y z : A} (p : x ≡ y) (q : y ≡ z) : x ≡ z :=
(* match p, q with refl, refl => refl end. *)
match p, q with eq_refl, eq_refl => eq_refl end.
Arguments Econcat {A x y z} p q : simpl nomatch.
Notation "'E1'" := eq_refl : eq_scope.
Notation "p E@ q" := (Econcat p%eq q%eq) (at level 20) : eq_scope.
Notation "p ^E" := (Einverse p%eq) (at level 3, format "p '^E'") : eq_scope.
Definition Etransport {A : Type} (P : A -> Type) {x y : A} (p : x ≡ y) (u : P x) : P y :=
match p with eq_refl => u end.
Arguments Etransport {A}%type_scope P {x y} p%eq_scope u : simpl nomatch.
Notation "p E# x"
:= (Etransport _ p x) (right associativity, at level 65, only parsing) : eq_scope.
Notation "f ≡≡ g" := (forall x, f x ≡ g x) (at level 70, no associativity) : type_scope.
Definition Eap {A B:Type} (f:A -> B) {x y:A} (p:x ≡ y) : f x ≡ f y
:= match p with eq_refl => eq_refl end.
Global Arguments Eap {A B}%type_scope f {x y} p%eq_scope.
Definition EapD10 {A} {B: A -> Type} {f g: forall x, B x} (h: f ≡ g)
: f ≡≡ g
:= fun x => match h with eq_refl => E1 end.
Global Arguments EapD10 {A%type_scope B} {f g} h%eq_scope _.
Definition Eap10 {A B} {f g: A -> B} (h: f ≡ g) : f ≡≡ g
:= EapD10 h.
Global Arguments Eap10 {A B}%type_scope {f g} h%eq_scope _.
Axiom eq_funext: forall {A: Type} {P : A -> Type} {f g : forall x : A, P x},
f ≡≡ g -> f ≡ g.