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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
|
(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
Set Primitive Projections.
Set Warnings "+non-primitive-record".
Set Warnings "+bad-relevance".
Check SProp.
Definition iUnit : SProp := forall A : SProp, A -> A.
Definition itt : iUnit := fun A a => a.
Definition iUnit_irr (P : iUnit -> Type) (x y : iUnit) : P x -> P y
:= fun v => v.
Definition iSquash (A:Type) : SProp
:= forall P : SProp, (A -> P) -> P.
Definition isquash A : A -> iSquash A
:= fun a P f => f a.
Definition iSquash_rect A (P : iSquash A -> SProp) (H : forall x : A, P (isquash A x))
: forall x : iSquash A, P x
:= fun x => x (P x) (H : A -> P x).
Fail Check (fun A : SProp => A : Type).
Lemma foo : Prop.
Proof. pose (fun A : SProp => ltac:(exact_no_check A): Type); exact True. Fail Qed. Abort.
(* define evar as product *)
Check (fun (f:(_:SProp)) => f _).
Inductive sBox (A:SProp) : Prop
:= sbox : A -> sBox A.
Definition uBox := sBox iUnit.
Definition sBox_irr A (x y : sBox A) : x = y.
Proof.
Fail reflexivity.
destruct x as [x], y as [y].
reflexivity.
Defined.
(* Primitive record with all fields in SProp has the eta property of SProp so must be SProp. *)
Fail Record rBox (A:SProp) : Prop := rmkbox { runbox : A }.
Section Opt.
Local Unset Primitive Projections.
Record rBox (A:SProp) : Prop := rmkbox { runbox : A }.
End Opt.
(* Check that defining as an emulated record worked *)
Check runbox.
(* Check that it doesn't have eta *)
Fail Check (fun (A : SProp) (x : rBox A) => eq_refl : x = @rmkbox _ (@runbox _ x)).
Inductive sEmpty : SProp := .
Inductive sUnit : SProp := stt.
Inductive BIG : SProp := foo | bar.
Inductive Squash (A:Type) : SProp
:= squash : A -> Squash A.
Definition BIG_flip : BIG -> BIG.
Proof.
intros [|]. exact bar. exact foo.
Defined.
Inductive pb : Prop := pt | pf.
Definition pb_big : pb -> BIG.
Proof.
intros [|]. exact foo. exact bar.
Defined.
Fail Definition big_pb (b:BIG) : pb :=
match b return pb with foo => pt | bar => pf end.
Inductive which_pb : pb -> SProp :=
| is_pt : which_pb pt
| is_pf : which_pb pf.
Fail Definition pb_which b (w:which_pb b) : bool
:= match w with
| is_pt => true
| is_pf => false
end.
(* Non primitive because no arguments, but maybe we should allow it for sprops? *)
Fail Record UnitRecord : SProp := {}.
Section Opt.
Local Unset Primitive Projections.
Record UnitRecord' : SProp := {}.
End Opt.
Fail Scheme Induction for UnitRecord' Sort Set.
Record sProd (A B : SProp) : SProp := sPair { sFst : A; sSnd : B }.
Scheme Induction for sProd Sort Set.
Unset Primitive Projections.
Record sProd' (A B : SProp) : SProp := sPair' { sFst' : A; sSnd' : B }.
Set Primitive Projections.
Fail Scheme Induction for sProd' Sort Set.
Inductive Istrue : bool -> SProp := istrue : Istrue true.
Definition Istrue_sym (b:bool) := if b then sUnit else sEmpty.
Definition Istrue_to_sym b (i:Istrue b) : Istrue_sym b := match i with istrue => stt end.
(* We don't need primitive elimination to relevant types for this *)
Definition Istrue_rec (P:forall b, Istrue b -> Set) (H:P true istrue) b (i:Istrue b) : P b i.
Proof.
destruct b.
- exact_no_check H.
- apply sEmpty_rec. apply Istrue_to_sym in i. exact i.
Defined.
Check (fun P v (e:Istrue true) => eq_refl : Istrue_rec P v _ e = v).
Record Truepack := truepack { trueval :> bool; trueprop : Istrue trueval }.
Definition Truepack_eta (x : Truepack) (i : Istrue x) : x = truepack x i := @eq_refl Truepack x.
Class emptyclass : SProp := emptyinstance : forall A:SProp, A.
(** Sigma in SProp can be done through Squash and relevant sigma. *)
Definition sSigma (A:SProp) (B:A -> SProp) : SProp
:= Squash (@sigT (rBox A) (fun x => rBox (B (runbox _ x)))).
Definition spair (A:SProp) (B:A->SProp) (x:A) (y:B x) : sSigma A B
:= squash _ (existT _ (rmkbox _ x) (rmkbox _ y)).
Definition spr1 (A:SProp) (B:A->SProp) (p:sSigma A B) : A
:= let 'squash _ (existT _ x y) := p in runbox _ x.
Definition spr2 (A:SProp) (B:A->SProp) (p:sSigma A B) : B (spr1 A B p)
:= let 'squash _ (existT _ x y) := p return B (spr1 A B p) in runbox _ y.
(* it's SProp so it computes properly *)
(** Fixpoints on SProp values are only allowed to produce SProp results *)
Inductive sAcc (x:nat) : SProp := sAcc_in : (forall y, y < x -> sAcc y) -> sAcc x.
Definition sAcc_inv x (s:sAcc x) : forall y, y < x -> sAcc y.
Proof.
destruct s as [H]. exact H.
Defined.
Section sFix_fail.
Variable P : nat -> Type.
Variable F : forall x:nat, (forall y:nat, y < x -> P y) -> P x.
Fail Fixpoint sFix (x:nat) (a:sAcc x) {struct a} : P x :=
F x (fun (y:nat) (h: y < x) => sFix y (sAcc_inv x a y h)).
End sFix_fail.
Section sFix.
Variable P : nat -> SProp.
Variable F : forall x:nat, (forall y:nat, y < x -> P y) -> P x.
Fixpoint sFix (x:nat) (a:sAcc x) {struct a} : P x :=
F x (fun (y:nat) (h: y < x) => sFix y (sAcc_inv x a y h)).
End sFix.
(** Relevance repairs *)
Definition fix_relevance : _ -> nat := fun _ : iUnit => 0.
Definition relevance_unfixed := fun (A:SProp) (P:A -> Prop) x y (v:P x) => v : P y.
(* The kernel is fine *)
Definition relevance_unfixed_bypass := fun (A:SProp) (P:A -> Prop) x y (v:P x) =>
ltac:(exact_no_check v) : P y.
(* Check that VM/native properly keep the relevance of the predicate in the case info
(bad-relevance warning as error otherwise) *)
Definition vm_rebuild_case := Eval vm_compute in eq_sind.
Require Import ssreflect.
Goal forall T : SProp, T -> True.
Proof.
move=> T +.
intros X;exact I.
Qed.
|
