Finish PER transitivity (#49)

theories/Core/Semantic/PERLemmas.v

@@ -118,6 +118,22 @@ Proof.
   intros. eauto using per_univ_elem_right_irrel_gen.
 Qed.
 
+Ltac per_univ_elem_right_irrel_rewrite :=
+  repeat match goal with
+    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
+        mark H2
+    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+        assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; mark H2
+    end; unmark_all.
+
+Ltac functional_per_univ_elem_rewrite_clear :=
+  repeat match goal with
+    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
+        clear H2
+    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+        assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; clear H2
+    end.
+
 Lemma per_univ_elem_sym : forall i A B R,
     per_univ_elem i A B R ->
     exists R', per_univ_elem i B A R' /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R' }}).
@@ -162,24 +178,100 @@ Proof.
     + intros; split; mauto.
 Qed.
 
-(* Lemma per_univ_elem_trans : forall i A1 A2 R1, *)
-(*     per_univ_elem i A1 A2 R1 -> *)
-(*     forall A3 R2, *)
-(*     per_univ_elem i A2 A3 R2 -> *)
-(*     exists R3, per_univ_elem i A1 A3 R3 /\ (forall a1 a2 a3, R1 a1 a2 -> R2 a2 a3 -> R3 a1 a3). *)
-(* Proof. *)
-(*   induction 1 using per_univ_elem_ind; intros ? ? HT2; *)
-(*     invert_per_univ_elem HT2. *)
-(*   - exists (per_univ j'0). *)
-(*     split. *)
-(*     + apply per_univ_elem_core_univ'; trivial. *)
-(*     + intros. unfold per_univ in *. *)
-(*       destruct H0, H2. *)
-(*       destruct (H1 _ _ _ H0 _ _ H2) as [? [? ?]]. *)
-(*       eauto. *)
-(*   - exists per_nat. *)
-(*     split... *)
-(*     + mauto. *)
-(*     + eapply per_nat_trans. *)
-(*   - specialize (IHper_univ_elem _ _ equiv_a_a'). *)
-(*     destruct IHper_univ_elem as [in_rel3 [? ?]]. *)
+Lemma per_univ_elem_left_irrel : forall i A B R A' R',
+    per_univ_elem i A B R ->
+    per_univ_elem i A' B R' ->
+    R = R'.
+Proof.
+  intros * [? []]%per_univ_elem_sym [? []]%per_univ_elem_sym.
+  per_univ_elem_right_irrel_rewrite.
+  extensionality a.
+  extensionality b.
+  specialize (H0 a b).
+  specialize (H2 a b).
+  apply propositional_extensionality; firstorder.
+Qed.
+
+Ltac per_univ_elem_left_irrel_rewrite :=
+  repeat match goal with
+    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A' ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
+        mark H2
+    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A' ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+        assert (R2 = R1) by (eapply per_univ_elem_left_irrel; eassumption); subst; mark H2
+    end; unmark_all.
+
+Ltac per_univ_elem_irrel_rewrite := functional_per_univ_elem_rewrite_clear; per_univ_elem_right_irrel_rewrite; per_univ_elem_left_irrel_rewrite.
+
+Lemma per_univ_elem_trans : forall i A1 A2 R1,
+    per_univ_elem i A1 A2 R1 ->
+    forall A3 R2,
+    per_univ_elem i A2 A3 R2 ->
+    exists R3, per_univ_elem i A1 A3 R3 /\ (forall a1 a2 a3, R1 a1 a2 -> R2 a2 a3 -> R3 a1 a3).
+Proof with solve [mauto].
+  induction 1 using per_univ_elem_ind; intros * HT2;
+    invert_per_univ_elem HT2; clear HT2.
+  - exists (per_univ j'0).
+    split; mauto.
+    intros.
+    destruct H0, H2.
+    destruct (H1 _ _ _ H0 _ _ H2) as [? [? ?]].
+    econstructor...
+  - exists per_nat.
+    split; try econstructor...
+  - rename R2 into elem_rel0.
+    destruct (IHper_univ_elem _ _ equiv_a_a') as [in_rel3 [? in_rel_trans]].
+    per_univ_elem_irrel_rewrite.
+    pose proof (per_univ_elem_sym _ _ _ _ H) as [in_rel' [? in_rel_sym]].
+    specialize (IHper_univ_elem _ _ H3) as [in_rel'' [? _]].
+    per_univ_elem_irrel_rewrite.
+    rename in_rel0 into in_rel.
+    assert (in_rel_refl : forall c c', in_rel c c' -> in_rel c' c').
+    {
+      intros.
+      assert (equiv_c'_c : in_rel c' c) by (destruct in_rel_sym with c c'; mauto)...
+    }
+    assert (forall (c c' : domain) (equiv_c_c' : in_rel c c'),
+             exists R3,
+               rel_mod_eval
+                 (fun (x y : domain) (R : relation domain) =>
+                    per_univ_elem i x y R)
+                 B d{{{ p ↦ c }}} B'0 d{{{ p'0 ↦ c' }}} R3
+               /\ (forall c'' (equiv_c_c'' : in_rel c c'') (equiv_c''_c' : in_rel c'' c') b0 b1 b2,
+                      out_rel _ _ equiv_c_c'' b0 b1 -> out_rel0 _ _ equiv_c''_c' b1 b2 -> R3 b0 b2)).
+    {
+      intros.
+      assert (equiv_c'_c' : in_rel c' c') by mauto.
+      destruct (H0 _ _ equiv_c_c') as [? ? ? ? []].
+      destruct (H7 _ _ equiv_c'_c') as [].
+      functional_eval_rewrite_clear.
+      destruct (H10 _ _ H13) as [R []].
+      exists R.
+      split.
+      - econstructor...
+      - intros.
+        specialize (H0 _ _ equiv_c_c'') as [? ? ? ? []].
+        specialize (H7 _ _ equiv_c''_c') as [].
+        functional_eval_rewrite_clear.
+        specialize (H19 _ _ H21) as [R' []].
+        per_univ_elem_irrel_rewrite.
+        eapply H7...
+    }
+    repeat setoid_rewrite dep_functional_choice_equiv in H5.
+    destruct H5 as [out_rel3 ?].
+    exists (fun f f' => forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel3 c c' equiv_c_c') f c f' c').
+    split.
+    + per_univ_elem_econstructor; mauto.
+      intros.
+      specialize (H5 _ _ equiv_c_c') as []...
+    + intros.
+      assert (equiv_c'_c' : in_rel c' c') by mauto.
+      rewrite H1 in H6.
+      rewrite H8 in H9.
+      specialize (H6 _ _ equiv_c_c') as [].
+      specialize (H9 _ _ equiv_c'_c') as [].
+      functional_eval_rewrite_clear.
+      specialize (H5 _ _ equiv_c_c') as [].
+      econstructor...
+  - exists per_ne.
+    split; try per_univ_elem_econstructor...
+Qed.