From 1a508ac3f2a25eec9e98d7b2b3e36de88d4e88b3 Mon Sep 17 00:00:00 2001 From: Junyoung/Clare Jang Date: Wed, 8 May 2024 19:12:38 -0400 Subject: [PATCH] Prove PER of per_ctx_env --- theories/Core/Semantic/PER.v | 2 +- theories/Core/Semantic/PERDefinitions.v | 97 +++++++++---------- theories/Core/Semantic/PERLemmas.v | 119 ++++++++++++++++++++++++ theories/_CoqProject | 1 + 4 files changed, 164 insertions(+), 55 deletions(-) create mode 100644 theories/Core/Semantic/PERLemmas.v diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v index 592bd696..e749f9a8 100644 --- a/theories/Core/Semantic/PER.v +++ b/theories/Core/Semantic/PER.v @@ -1 +1 @@ -From Mcltt Require Export PERBasicLemmas PERDefinitions. +From Mcltt Require Export PERDefinitions PERLemmas. diff --git a/theories/Core/Semantic/PERDefinitions.v b/theories/Core/Semantic/PERDefinitions.v index e0ac8419..de2e898d 100644 --- a/theories/Core/Semantic/PERDefinitions.v +++ b/theories/Core/Semantic/PERDefinitions.v @@ -77,7 +77,9 @@ Inductive per_ne : relation domain := (** Universe/Element PER Definition *) Section Per_univ_elem_core_def. - Variable (i : nat) (per_univ_rec : forall {j}, j < i -> relation domain). + Variable + (i : nat) + (per_univ_rec : forall {j}, j < i -> relation domain). Inductive per_univ_elem_core : domain -> domain -> relation domain -> Prop := | per_univ_elem_core_univ : @@ -100,28 +102,20 @@ Section Per_univ_elem_core_def. . Hypothesis - (motive : domain -> domain -> relation domain -> Prop). - - Hypothesis - (case_U : forall (j j' : nat) (lt_j_i : j < i), j = j' -> motive d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ_rec lt_j_i)). - - Hypothesis - (case_nat : motive d{{{ ℕ }}} d{{{ ℕ }}} per_nat). - - Hypothesis - (case_Pi : - forall {A p B A' p' B' in_rel elem_rel} - (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain), - {{ DF A ≈ A' ∈ per_univ_elem_core ↘ in_rel }} -> - motive A A' in_rel -> - PER in_rel -> - (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), - rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem_core ↘ R }} /\ motive x y R) 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' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') -> - motive d{{{ Π A p B }}} d{{{ Π A' p' B' }}} elem_rel). - - Hypothesis - (case_ne : (forall {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}} per_ne)). + (motive : domain -> domain -> relation domain -> Prop) + (case_U : forall (j j' : nat) (lt_j_i : j < i), j = j' -> motive d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ_rec lt_j_i)) + (case_nat : motive d{{{ ℕ }}} d{{{ ℕ }}} per_nat) + (case_Pi : + forall {A p B A' p' B' in_rel elem_rel} + (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain), + {{ DF A ≈ A' ∈ per_univ_elem_core ↘ in_rel }} -> + motive A A' in_rel -> + PER in_rel -> + (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), + rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem_core ↘ R }} /\ motive x y R) 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' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') -> + motive d{{{ Π A p B }}} d{{{ Π A' p' B' }}} elem_rel) + (case_ne : (forall {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}} per_ne)). #[derive(equations=no, eliminator=no)] Equations per_univ_elem_core_strong_ind a b R (H : {{ DF a ≈ b ∈ per_univ_elem_core ↘ R }}) : {{ DF a ≈ b ∈ motive ↘ R }} := @@ -163,30 +157,22 @@ Global Hint Resolve per_univ_elem_core_univ' : mcltt. Section Per_univ_elem_ind_def. Hypothesis - (motive : nat -> domain -> domain -> relation domain -> Prop). - - Hypothesis - (case_U : forall j j' i, j < i -> j = j' -> - (forall A B R, {{ DF A ≈ B ∈ per_univ_elem j ↘ R }} -> motive j A B R) -> - motive i d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ j)). - - Hypothesis - (case_N : forall i, motive i d{{{ ℕ }}} d{{{ ℕ }}} per_nat). - - Hypothesis - (case_Pi : - forall i {A p B A' p' B' in_rel elem_rel} - (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain), - {{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel }} -> - motive i A A' in_rel -> - PER in_rel -> - (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), - rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem i ↘ R }} /\ motive i x y R) 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' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') -> - motive i d{{{ Π A p B }}} d{{{ Π A' p' B' }}} elem_rel). - - Hypothesis - (case_ne : (forall i {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive i d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}} per_ne)). + (motive : nat -> domain -> domain -> relation domain -> Prop) + (case_U : forall j j' i, j < i -> j = j' -> + (forall A B R, {{ DF A ≈ B ∈ per_univ_elem j ↘ R }} -> motive j A B R) -> + motive i d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ j)) + (case_N : forall i, motive i d{{{ ℕ }}} d{{{ ℕ }}} per_nat) + (case_Pi : + forall i {A p B A' p' B' in_rel elem_rel} + (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain), + {{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel }} -> + motive i A A' in_rel -> + PER in_rel -> + (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), + rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem i ↘ R }} /\ motive i x y R) 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' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') -> + motive i d{{{ Π A p B }}} d{{{ Π A' p' B' }}} elem_rel) + (case_ne : (forall i {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive i d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}} per_ne)). #[local] Ltac def_simp := simp per_univ_elem in *. @@ -225,18 +211,21 @@ Ltac per_univ_elem_econstructor := 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'. +Definition per_total : relation env := fun p p' => True. + Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop := | per_ctx_env_nil : - `{ (Env = fun p p' => True) -> - {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ Env }} } + `{ {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ per_total }} } | per_ctx_env_cons : `{ forall (tail_rel : relation env) - (head_rel : forall {p p'}, {{ Dom p ≈ p' ∈ tail_rel }} -> relation domain) + (head_rel : forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), relation domain) (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 }} } + PER 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_rel = 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_rel }} } . Definition per_ctx : relation ctx := fun Γ Γ' => exists R', per_ctx_env Γ Γ' R'. diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v new file mode 100644 index 00000000..552bbad1 --- /dev/null +++ b/theories/Core/Semantic/PERLemmas.v @@ -0,0 +1,119 @@ +From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses. +From Mcltt Require Import Axioms Base Evaluation LibTactics PERDefinitions. +From Mcltt Require Export PERBasicLemmas. +Import Domain_Notations. + +Lemma per_ctx_env_right_irrel : forall Γ Δ Δ' R R', + {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} -> + {{ DF Γ ≈ Δ' ∈ per_ctx_env ↘ R' }} -> + R = R'. +Proof. + intros * Horig; gen Δ' R'. + induction Horig; intros * Hright; + try solve [inversion Hright; congruence]. + subst. + inversion_clear Hright. + specialize (IHHorig _ _ equiv_Γ_Γ'0). + subst. + enough (head_rel = head_rel0) by (subst; easy). + extensionality p. + extensionality p'. + extensionality equiv_p_p'. + unfold rel_typ in *. + destruct_rel_mod_eval. + per_univ_elem_irrel_rewrite. + congruence. +Qed. + +Lemma per_ctx_env_sym : forall Γ Δ R, + {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} -> + {{ DF Δ ≈ Γ ∈ per_ctx_env ↘ R }} /\ (forall o p, {{ Dom o ≈ p ∈ R }} -> {{ Dom p ≈ o ∈ R }}). +Proof with solve [eauto]. + simpl. + induction 1; firstorder; try solve [econstructor; eauto]; unfold rel_typ in *. + - econstructor; eauto; firstorder. + assert (tail_rel p' p) by eauto. + assert (tail_rel p p) by (etransitivity; eauto). + destruct_rel_mod_eval. + per_univ_elem_irrel_rewrite. + econstructor; eauto. + apply per_univ_elem_sym... + - subst. + firstorder. + assert (tail_rel d{{{ p ↯ }}} d{{{ o ↯ }}}) by (unfold Symmetric in *; eauto). + assert (tail_rel d{{{ p ↯ }}} d{{{ p ↯ }}}) by (etransitivity; eauto). + destruct_rel_mod_eval. + eexists. + per_univ_elem_irrel_rewrite. + eapply per_univ_elem_sym... +Qed. + +Lemma per_ctx_env_left_irrel : forall Γ Γ' Δ R R', + {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} -> + {{ DF Γ' ≈ Δ ∈ per_ctx_env ↘ R' }} -> + R = R'. +Proof. + intros * []%per_ctx_env_sym []%per_ctx_env_sym. + eauto using per_ctx_env_right_irrel. +Qed. + +Lemma per_ctx_env_cross_irrel : forall Γ Δ Δ' R R', + {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} -> + {{ DF Δ' ≈ Γ ∈ per_ctx_env ↘ R' }} -> + R = R'. +Proof. + intros * ? []%per_ctx_env_sym. + eauto using per_ctx_env_right_irrel. +Qed. + +Ltac do_per_ctx_env_irrel_rewrite1 := + match goal with + | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }}, + H2 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R2 }} |- _ => + clean replace R2 with R1 by (eauto using per_ctx_env_right_irrel) + | H1 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R1 }}, + H2 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R2 }} |- _ => + clean replace R2 with R1 by (eauto using per_ctx_env_left_irrel) + | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }}, + H2 : {{ DF ~_ ≈ ~?Γ ∈ per_ctx_env ↘ ?R2 }} |- _ => + (* Order matters less here as H1 and H2 cannot be exchanged *) + clean replace R2 with R1 by (symmetry; eauto using per_ctx_env_cross_irrel) + end. + +Ltac do_per_ctx_env_irrel_rewrite := + repeat do_per_ctx_env_irrel_rewrite1. + +Ltac per_ctx_env_irrel_rewrite := + functional_eval_rewrite_clear; + do_per_ctx_env_irrel_rewrite; + clear_dups. + +Lemma per_ctx_env_trans : forall Γ1 Γ2 R, + {{ DF Γ1 ≈ Γ2 ∈ per_ctx_env ↘ R }} -> + forall Γ3, + {{ DF Γ2 ≈ Γ3 ∈ per_ctx_env ↘ R }} -> + {{ DF Γ1 ≈ Γ3 ∈ per_ctx_env ↘ R }} /\ (forall p1 p2 p3, {{ Dom p1 ≈ p2 ∈ R }} -> {{ Dom p2 ≈ p3 ∈ R }} -> {{ Dom p1 ≈ p3 ∈ R }}). +Proof with solve [eauto]. + simpl. + induction 1; intros * HTrans23; inversion HTrans23; subst; eauto. + per_ctx_env_irrel_rewrite. + rename tail_rel0 into tail_rel. + split. + - econstructor; eauto. + + eapply IHper_ctx_env... + + unfold rel_typ in *. + intros. + assert (tail_rel p p) by (etransitivity; [ | symmetry]; eassumption). + destruct_rel_mod_eval. + econstructor; eauto. + per_univ_elem_irrel_rewrite. + eapply proj1, per_univ_elem_trans; [|eassumption]... + - intros * [] []. + specialize (IHper_ctx_env _ equiv_Γ_Γ'0) as []. + assert (tail_rel d{{{ p1 ↯ }}} d{{{ p3 ↯ }}}) by eauto. + eexists. + unfold rel_typ in *. + destruct_rel_mod_eval. + per_univ_elem_irrel_rewrite. + eapply per_univ_elem_trans... +Qed. diff --git a/theories/_CoqProject b/theories/_CoqProject index 8eb2eef6..7520ea58 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -11,6 +11,7 @@ ./Core/Semantic/PER.v ./Core/Semantic/PERBasicLemmas.v ./Core/Semantic/PERDefinitions.v +./Core/Semantic/PERLemmas.v ./Core/Semantic/Readback.v ./Core/Semantic/ReadbackDefinitions.v ./Core/Semantic/ReadbackLemmas.v