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
|
From stdpp Require Import numbers option sorting ssreflect.
From stdpp Require Import options.
Definition transportf {X} (P : X → Type) {x x' : X} : x = x' → P x → P x'.
Proof. by induction 1. Defined.
Instance HdRel_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} a l : ProofIrrel (HdRel R a l).
Proof.
intros HR1 HR2.
assert (Hnil : ∀ xs (Hxs : [] = xs) (HR : HdRel R a xs),
HR = transportf _ Hxs (HdRel_nil R a)).
{ intros. destruct HR; last done.
by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
assert (Hcons : ∀ xs x y xs' (Hxs : y :: xs' = xs) (HR : HdRel R x xs) (Hxy : R x y),
HR = transportf (HdRel R x) Hxs (HdRel_cons R x y xs' Hxy)).
{ intros. destruct HR; first done.
injection Hxs as <- <-.
replace Hxs with (eq_refl (y :: xs')); last apply eq_pi, list_eq_dec.
simpl.
by replace r with Hxy by apply H. }
destruct l.
- trans (transportf (HdRel R a) eq_refl (HdRel_nil R a)).
+ apply Hnil.
+ symmetry. apply Hnil.
- apply HdRel_inv in HR1 as Haa0.
trans (transportf (HdRel R a) eq_refl (HdRel_cons R a a0 l Haa0)).
+ apply Hcons.
+ symmetry. apply Hcons.
Qed.
Instance Sorted_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} l : ProofIrrel (Sorted R l).
Proof.
intros HS1 HS2.
assert (Hbase : ∀ xs (Hxs : [] = xs) (HS : Sorted R xs), HS = transportf _ Hxs (Sorted_nil R)).
{ intros. destruct HS; last done.
by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
assert (Hind : ∀ xs x xs'
(Hxs : x :: xs' = xs) (HS : Sorted R xs)
(Hx : HdRel R x xs') (HS' : Sorted R xs')
(IH : ∀ HS1' HS2' : Sorted R xs', HS1' = HS2'),
HS = transportf _ Hxs (Sorted_cons HS' Hx)).
{ intros. destruct HS; first done.
injection Hxs as <- <-.
replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
simpl.
replace h with Hx by apply: HdRel_pi.
by replace HS with HS' by apply IH. }
induction l.
- trans (transportf _ eq_refl (Sorted_nil R)).
+ apply Hbase.
+ symmetry. apply Hbase.
- destruct (Sorted_inv HS1) as [Hl Hal].
trans (transportf _ eq_refl (Sorted_cons Hl Hal)).
+ apply Hind, IHl.
+ symmetry. apply Hind, IHl.
Qed.
Instance Forall_pi {A} (P : A → Prop) (l : list A) `{!EqDecision A} `{!∀ a, ProofIrrel (P a)} : ProofIrrel (Forall P l).
Proof.
intros HF1 HF2.
assert (Hbase : ∀ xs (Hxs : [] = xs) (HF : Forall P xs), HF = transportf (Forall P) Hxs (ListDef.Forall_nil P)).
{ intros xs Hxs HF. destruct HF; last done.
by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
assert (Hind : ∀ xs x xs'
(Hxs : x :: xs' = xs) (HF : Forall P xs)
(Hx : P x) (HF' : Forall P xs')
(IH : ∀ HF1' HF2' : Forall P xs', HF1' = HF2'),
HF = transportf _ Hxs (ListDef.Forall_cons P x xs' Hx HF')).
{ intros. destruct HF; first done.
injection Hxs as <- <-.
replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
simpl.
replace p with Hx by apply H.
by replace HF with HF' by apply IH. }
induction l.
- trans (transportf _ eq_refl (ListDef.Forall_nil P)).
+ apply Hbase.
+ symmetry. apply Hbase.
- apply Forall_inv in HF1 as Ha.
apply Forall_inv_tail in HF1 as Hl.
trans (transportf _ eq_refl (ListDef.Forall_cons P a l Ha Hl)).
+ apply Hind, IHl.
+ symmetry. apply Hind, IHl.
Qed.
Instance ex_pi {A} {B : A → Prop} `{!ProofIrrel A} `{!∀ x, ProofIrrel (B x)} :
ProofIrrel (∃ (x : A), B x).
Proof.
intros [x Hx] [y Hy].
assert (y = x) by apply proof_irrel. subst.
assert (Hx = Hy) by apply proof_irrel. by subst.
Qed.
|
