/
sprop_uip.v
127 lines (97 loc) · 3.39 KB
/
sprop_uip.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
126
127
Set Allow StrictProp.
Set Definitional UIP.
Set Warnings "+bad-relevance".
(** Case inversion, conversion and universe polymorphism. *)
Set Universe Polymorphism.
Inductive IsTy@{i j} : Type@{j} -> SProp :=
isty : IsTy Type@{i}.
Definition IsTy_rec_red@{i j+} (P:forall T : Type@{j}, IsTy@{i j} T -> Set)
v (e:IsTy@{i j} Type@{i})
: IsTy_rec P v _ e = v
:= eq_refl.
(** Identity! Currently we have UIP. *)
Inductive seq {A} (a:A) : A -> SProp :=
srefl : seq a a.
Definition transport {A} (P:A -> Type) {x y} (e:seq x y) (v:P x) : P y :=
match e with
srefl _ => v
end.
Definition transport_refl {A} (P:A -> Type) {x} (e:seq x x) v
: transport P e v = v
:= @eq_refl (P x) v.
Definition id_unit (x : unit) := x.
Definition transport_refl_id {A} (P : A -> Type) {x : A} (u : P x)
: P (transport (fun _ => A) (srefl _ : seq (id_unit tt) tt) x)
:= u.
(** We don't ALWAYS reduce (this uses a constant transport so that the
equation is well-typed) *)
Fail Definition transport_block A B (x y:A) (e:seq x y) v
: transport (fun _ => B) e v = v
:= @eq_refl B v.
Inductive sBox (A:SProp) : Prop
:= sbox : A -> sBox A.
Definition transport_refl_box (A:SProp) P (x y:A) (e:seq (sbox A x) (sbox A y)) v
: transport P e v = v
:= eq_refl.
(** TODO? add tests for binders which aren't lambda. *)
Definition transport_box :=
Eval lazy in (fun (A:SProp) P (x y:A) (e:seq (sbox A x) (sbox A y)) v =>
transport P e v).
Lemma transport_box_ok : transport_box = fun A P x y e v => v.
Proof.
unfold transport_box.
match goal with |- ?x = ?x => reflexivity end.
Qed.
(** Play with UIP *)
Lemma of_seq {A:Type} {x y:A} (p:seq x y) : x = y.
Proof.
destruct p. reflexivity.
Defined.
Lemma to_seq {A:Type} {x y:A} (p: x = y) : seq x y.
Proof.
destruct p. reflexivity.
Defined.
Lemma eq_srec (A:Type) (x y:A) (P:x=y->Type) : (forall e : seq x y, P (of_seq e)) -> forall e, P e.
Proof.
intros H e. destruct e.
apply (H (srefl _)).
Defined.
Lemma K : forall {A x} (p:x=x:>A), p = eq_refl.
Proof.
intros A x. apply eq_srec. intros;reflexivity.
Defined.
Definition K_refl : forall {A x}, @K A x eq_refl = eq_refl
:= fun A x => eq_refl.
Section funext.
Variable sfunext : forall {A B} (f g : A -> B), (forall x, seq (f x) (g x)) -> seq f g.
Lemma funext {A B} (f g : A -> B) (H:forall x, (f x) = (g x)) : f = g.
Proof.
apply of_seq,sfunext;intros x;apply to_seq,H.
Defined.
Definition funext_refl A B (f : A -> B) : funext f f (fun x => eq_refl) = eq_refl
:= eq_refl.
End funext.
(* test reductions on inverted cases *)
(* first check production of correct blocked cases *)
Definition lazy_seq_rect := Eval lazy in seq_rect.
Definition vseq_rect := Eval vm_compute in seq_rect.
Definition native_seq_rect := Eval native_compute in seq_rect.
Definition cbv_seq_rect := Eval cbv in seq_rect.
(* check it reduces according to indices *)
Ltac reset := match goal with H : _ |- _ => change (match H with srefl _ => False end) end.
Ltac check := match goal with |- False => idtac end.
Lemma foo (H:seq 0 0) : False.
Proof.
reset.
Fail check. (* check that "reset" and "check" actually do something *)
lazy; check; reset.
(* TODO *)
vm_compute. Fail check.
native_compute. Fail check.
cbv. Fail check.
cbn. Fail check.
simpl. Fail check.
Abort.
(* check that extraction doesn't fall apart on matches with special reduction *)
Require Extraction.
Extraction seq_rect.