Merge branch 'pr-domain-definition' of github.com:Beluga-lang/McLTT i…

…nto pr-domain-definition

theories/Core/Semantic/PER.v

@@ -1,4 +1,9 @@
 From Coq Require Import Lia PeanoNat Relations.
+<<<<<<< HEAD
+=======
+From Equations Require Import Equations.
+
+>>>>>>> 47fa52f5eb989104966e70555de900ab7ce0e164
 From Mcltt Require Import Base Domain Evaluate Readback Syntax System.
 From Equations Require Import Equations.
 
@@ -53,8 +58,13 @@ Section Per_univ_elem_core_def.
   | per_univ_elem_core_nat : {{ DF ℕ ≈ ℕ ∈ per_univ_elem_core ↘ per_nat }}
   | per_univ_elem_core_pi :
     `{ forall (in_rel : relation domain)
+<<<<<<< HEAD
          (out_rel : forall {c c'}, {{ Dom c ≈ c' ∈ in_rel }} -> relation domain)
          (equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel}}),
+=======
+          (out_rel : forall {c c'}, {{ Dom c ≈ c' ∈ in_rel }} -> relation domain)
+          (equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel }}),
+>>>>>>> 47fa52f5eb989104966e70555de900ab7ce0e164
           (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
               rel_mod_eval per_univ_elem_core B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
           (forall f f', elem_rel f f' <-> forall {c c'} (equiv_c_c' : in_rel c c'),
@@ -108,6 +118,7 @@ Global Hint Constructors per_univ_elem_core : mcltt.
 
 Equations per_univ_elem (i : nat) : domain -> domain -> relation domain -> Prop by wf i :=
 | i => per_univ_elem_core i (fun j lt_j_i a a' => exists R', per_univ_elem j a a' R').
+<<<<<<< HEAD
 
 Definition per_univ (i : nat) : relation domain := fun a a' => exists R', per_univ_elem i a a' R'.
 
@@ -175,6 +186,10 @@ Definition per_univ_like (R : domain -> domain -> relation domain -> Prop) := fu
 #[global]
 Transparent per_univ_like.
 
+=======
+Definition per_univ (i : nat) : relation domain := fun a a' => exists R', per_univ_elem i a a' R'.
+
+>>>>>>> 47fa52f5eb989104966e70555de900ab7ce0e164
 Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
 
 Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=
@@ -184,8 +199,8 @@ Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=
 | per_ctx_env_cons :
   `{ forall (tail_rel : relation env)
         (head_rel : forall {p p'}, {{ Dom p ≈ p' ∈ tail_rel }} -> relation domain)
-        (equiv_Γ_Γ' : {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ tail_rel }})
-        (rel_A_A' : forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), rel_typ i A p A' p' (head_rel equiv_p_p')),
+        (equiv_Γ_Γ' : {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ tail_rel }}),
+        (forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), rel_typ i A p A' p' (head_rel equiv_p_p')) ->
         (Env = fun p p' => exists (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ tail_rel }}),
                    {{ Dom ~(p 0) ≈ ~(p' 0) ∈ head_rel equiv_p_drop_p'_drop }}) ->
         {{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ Env }} }

theories/Core/Semantic/PERLemmas.v

@@ -1,5 +1,6 @@
 From Coq Require Import Lia PeanoNat Relations Program.Equality.
 From Mcltt Require Import Axioms Base Domain Evaluate LibTactics PER Readback Syntax System.
+From Equations Require Import Equations.
 
 Lemma per_univ_elem_sym : forall i A B R,
     per_univ_elem i A B R ->
@@ -121,37 +122,42 @@ Proof.
 (* Qed. *)
 
 Lemma per_univ_sym : forall m m' i,
-    {{ Dom m ≈ m' ∈ per_univ i }} ->
-    {{ Dom m' ≈ m ∈ per_univ i }}
-with per_elem_sym : forall m m' i R R'
+    {{ Dom m ≈ m' ∈ per_univ i }} -> {{ Dom m' ≈ m ∈ per_univ i }}
+with per_elem_sym : forall m m' i R R' a a'
   (equiv_m_m' : {{ DF m ≈ m' ∈ per_univ_elem i ↘ R }})
   (equiv_m'_m : {{ DF m' ≈ m ∈ per_univ_elem i ↘ R' }}),
-    {{ Dom m ≈ m' ∈ R }} ->
-    {{ Dom m' ≈ m ∈ R' }}.
+    {{ Dom a ≈ a' ∈ R }} <-> {{ Dom a' ≈ a ∈ R' }}.
 Proof with mauto.
-  - intros.
-    destruct H as [per_elem Hper_univ].
-    unfold in_dom_fun_rel in *.
-    dependent induction Hper_univ; try solve [subst; eexists; econstructor; mauto].
-    + fold per_univ_elem in equiv_a_a'.
-    (*   eexists; econstructor... *)
-    (* +  *)
-    (* unfold per_univ, Per_univ_def.per_univ, in_dom_rel in *. *)
-    (* destruct H as [equiv_a_a' Hcheck]. *)
-    (* dependent induction Hcheck; subst. *)
-    (* + eexists. *)
-    (*   eapply Per_univ_def.per_univ_check_univ. *)
-    (*   Unshelve. all: auto. *)
-    (* + eexists. *)
-    (*   econstructor. *)
-    (* + destruct IHHcheck. *)
-    (*   assert (Per_univ_def.per_univ_template i d{{{ Π a' p' B'}}} d{{{ Π a p B}}}). *)
-    (*   { eapply (@Per_univ_def.per_univ_template_pi i _ _ _ _ _ _ (per_univ i) (fun _ _ => per_elem) (ex_intro _ x H1)). *)
-    (*     intros. *)
-    (*     unfold in_dom_rel, per_elem, Per_univ_def.per_elem in *. *)
-    (*   } *)
+  all: intros *; try split.
+  1: intro Hper_univ.
+  2-3: intro Hper_elem.
+  - destruct Hper_univ as [per_elem equiv_m_m'].
+    autorewrite with per_univ_elem in equiv_m_m'.
+    dependent induction equiv_m_m'; subst; only 1-2,4: solve [eexists; econstructor; mauto].
+    (* Pi case *)
+    destruct IHequiv_m_m' as [in_rel' IHequiv_a_a'].
+    rewrite <- per_univ_elem_equation_1 in H, equiv_a_a'.
+    (* (* One attempt *) *)
+    (* unshelve epose (out_rel' := _ : forall c' c : domain, {{ Dom c' ≈ c ∈ in_rel' }} -> relation domain). *)
+    (* { *)
+    (*   intros * equiv_c'_c. *)
+    (*   assert (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}) by (erewrite per_elem_sym; eassumption). *)
+    (*   assert (rel_mod_eval (per_univ_elem i) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel c c' equiv_c_c')) by mauto. *)
+    (*   (* Failure point *) *)
+    (*   destruct_last. *)
+    (* } *)
+
+    (* (* The other *) *)
+    (* assert (exists (out_rel' : forall c' c : domain, {{ Dom c' ≈ c ∈ in_rel' }} -> relation domain), *)
+    (*          forall (c' c : domain) (equiv_c'_c : {{ Dom c' ≈ c ∈ in_rel' }}), *)
+    (*            rel_mod_eval (per_univ_elem i) B' d{{{ p' ↦ c' }}} B d{{{ p ↦ c }}} (out_rel' c' c equiv_c'_c)). *)
+    (* { *)
+    (*   (* This "eexists" is problematic *) *)
     (*   eexists. *)
-    (*   econstructor. *)
-    (*   * eassumption. *)
-    (*   * intros. *)
+    (*   intros. *)
+    (*   assert (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}) by (erewrite per_elem_sym; eassumption). *)
+    (*   assert (rel_mod_eval (per_univ_elem i) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel c c' equiv_c_c')) by mauto. *)
+    (*   destruct_last. *)
+    (*   econstructor; try eassumption. *)
+    (* } *)