Import from e4b104792206ee7ea64bf39c6b7d2c0c230f9d14

1 files changed, 92 insertions, 0 deletions

diff --git a/server/formal/util.v b/server/formal/util.v
new file mode 100644
index 0000000..8e16ffc
--- /dev/null
+++ b/server/formal/util.v
@@ -0,0 +1,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.