Defer nat cases

Beluga-lang · May 22, 2024 · 960267f · 960267f
1 parent b080b96
commit 960267f
Showing 1 changed file with 45 additions and 34 deletions.
diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v
@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms_Relations Relation_Definitions RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases System.
 Import Domain_Notations.
 
 Lemma valid_exp_nat : forall {Γ i},
@@ -97,53 +97,69 @@ Proof.
   - econstructor; eassumption.
 Qed.
 
-Lemma rel_exp_natrec_cong : forall {Γ env_relΓ MZ MZ' MS MS' A A' i m m'},
+Lemma eval_natrec_rel : forall {Γ env_relΓ MZ MZ' MS MS' A A' i m m'},
     {{ DF Γ ≈ Γ ∈ per_ctx_env ↘ env_relΓ }} ->
     {{ Γ, ℕ ⊨ A ≈ A' : Type@i }} ->
     {{ Γ ⊨ MZ ≈ MZ' : A[Id,,zero] }} ->
     {{ Γ, ℕ, A ⊨ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
     {{ Dom m ≈ m' ∈ per_nat }} ->
     (forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
       forall (elem_rel : relation domain),
-        rel_typ i A p A p' elem_rel ->
+        rel_typ i A d{{{ p ↦ m }}} A d{{{ p' ↦ m' }}} elem_rel ->
         exists r r',
           {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} /\
             {{ rec m' ⟦return A' | zero -> MZ' | succ -> MS' end⟧ p' ↘ r' }} /\
             {{ Dom r ≈ r' ∈ elem_rel }}).
 Proof.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
-  intros * equiv_Γ_Γ [env_relΓℕ] [] [env_relΓℕA] equiv_m_m'.
+  intros * equiv_Γ_Γ HAA' [] [env_relΓℕA] equiv_m_m'.
+  assert {{ Γ, ℕ ⊨ A : Type@i }} as [env_relΓℕ] by (unfold valid_exp_under_ctx; etransitivity; [| symmetry]; eassumption).
   destruct_conjs.
   pose (env_relΓℕA0 := env_relΓℕA).
   pose (env_relΓℕ0 := env_relΓℕ).
-  match_by_head (per_ctx_env env_relΓℕA)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
-  destruct_conjs.
+  match_by_head (per_ctx_env env_relΓℕA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
-  match_by_head (per_ctx_env env_relΓℕ)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
-  destruct_conjs.
+  match_by_head (per_ctx_env env_relΓℕ) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
-  induction equiv_m_m'; intros; destruct_by_head rel_typ.
-  2: {
-    (on_all_hyp_rev: fun H => unshelve epose proof (H _ _ equiv_p_p' elem_rel _)).
-    + econstructor; mauto.
-    + destruct_conjs.
-      rename H20 into r0.
-      rename H21 into r'0.
-      (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-      invert_rel_typ_body.
-      assert {{ Dom p ↦ m ≈ p' ↦ n ∈ env_relΓℕ }} by (apply_relation_equivalence; eexists; eauto).
-  (*     assert {{ Dom p ↦ m ↦ r0 ≈ p' ↦ n ↦ r'0 ∈ env_relΓℕA }}. *)
-  (*     { *)
-  (*       apply_relation_equivalence; eexists; eauto. *)
-  (*     } *)
-  (*     do 2 eexists. *)
-  (*     repeat split; only 1-2: econstructor; eauto. *)
-  (* } *)
-  (* - (* zero *) *)
-  (*   (on_all_hyp: destruct_rel_by_assumption env_rel). *)
+  induction equiv_m_m'; intros;
+    destruct_by_head rel_typ;
+    (on_all_hyp: destruct_rel_by_assumption env_relΓ);
+    invert_rel_typ_body;
+    destruct_by_head rel_typ;
+    dir_inversion_by_head eval_exp; subst;
+    dir_inversion_by_head eval_sub; subst;
+    dir_inversion_by_head eval_exp; subst;
+    functional_eval_rewrite_clear;
+    destruct_by_head rel_exp;
+    handle_per_univ_elem_irrel.
+  - do 2 eexists.
+    repeat split; only 1-2: econstructor; eauto.
+  - assert {{ Dom p'2 ↦ m ≈ p'3 ↦ n ∈ env_relΓℕ }} by (apply_relation_equivalence; eexists; eauto).
+    (on_all_hyp: destruct_rel_by_assumption env_relΓℕ).
+    assert {{ Dom p'2 ↦ m ≈ p'3 ↦ n ∈ env_relΓℕ }} as HinΓℕ by (apply_relation_equivalence; eexists; eauto).
+    apply_relation_equivalence.
+    (on_all_hyp: fun H => directed destruct (H _ _ HinΓℕ) as [? []]).
+    destruct_by_head rel_typ.
+    invert_rel_typ_body.
+    destruct_by_head rel_exp.
+    destruct_conjs.
+    unshelve epose proof (IHequiv_m_m' _ _ equiv_p_p' _ _) as [? [? [? []]]]; [| econstructor; solve [eauto] |].
+    handle_per_univ_elem_irrel.
+    rename x4 into r0.
+    rename x5 into r'0.
+    assert {{ Dom p'2 ↦ m ↦ r0 ≈ p'3 ↦ n ↦ r'0 ∈ env_relΓℕA }} as HinΓℕA by (apply_relation_equivalence; eexists; eauto).
+    apply_relation_equivalence.
+    (on_all_hyp: fun H => directed destruct (H _ _ HinΓℕA) as [? []]).
+    destruct_by_head rel_typ.
+    invert_rel_typ_body.
+    destruct_by_head rel_exp.
+    dir_inversion_by_head eval_sub; subst.
+    dir_inversion_by_head (eval_exp {{{ zero }}}); subst.
+    dir_inversion_by_head (eval_exp {{{ succ #1 }}}); subst.
+    dir_inversion_by_head (eval_exp {{{ #1 }}}); subst.
+    match_by_head eval_exp ltac:(fun H => simpl in H).
+    clear_refl_eqs.
 Abort.
 
 Lemma rel_exp_natrec_cong : forall {Γ MZ MZ' MS MS' A A' i M M'},
@@ -182,8 +198,3 @@ Proof.
   destruct_by_head rel_exp.
   destruct_conjs.
   Abort.
-(*   eexists. *)
-(*   split; [> econstructor; only 1-2: repeat econstructor ..]; eauto. *)
-(*   - per_univ_elem_econstructor; reflexivity. *)
-(*   - econstructor; eassumption. *)
-(* Qed. *)