diff --git a/theories/logrel.v b/theories/logrel.v index 2c3a99e..6d9f628 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -1,4 +1,180 @@ Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. +Require Import fp_red. +From Hammer Require Import Tactics. +From Equations Require Import Equations. +Require Import ssreflect. +Require Import Logic.PropExtensionality (propositional_extensionality). +From stdpp Require Import relations (rtc(..)). Definition ProdSpace {n} (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop) : Tm n -> Prop := fun b => forall a PB, PA a -> PF a PB -> PB (App b a). + +Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70). +Inductive InterpExt {n} i (I : forall n, nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) -> Prop := +| InterpExt_Fun A B PA PF : + ⟦ A ⟧ i ;; I ↘ PA -> + (forall a, PA a -> exists PB, PF a PB) -> + (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) -> + ⟦ Pi A B ⟧ i ;; I ↘ (ProdSpace PA PF) + +| InterpExt_Univ j : + j < i -> + ⟦ Univ j ⟧ i ;; I ↘ (I n j) + +| InterpExt_Step A A0 PA : + RPar.R A A0 -> + ⟦ A0 ⟧ i ;; I ↘ PA -> + ⟦ A ⟧ i ;; I ↘ PA +where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S). + +Lemma InterpExt_Univ' {n} i I j (PF : Tm n -> Prop) : + PF = I n j -> + j < i -> + ⟦ Univ j ⟧ i ;; I ↘ PF. +Proof. hauto lq:on ctrs:InterpExt. Qed. + +Infix " (Tm n -> Prop) -> Prop by wf i lt := + InterpUnivN n i := @InterpExt n i + (fun n j A => + match j exists PA, InterpUnivN n j A PA + | right _ => False + end). +Arguments InterpUnivN {n}. + +Lemma InterpExt_lt_impl {n : nat} i I I' A (PA : Tm n -> Prop) : + (forall j, j < i -> I n j = I' n j) -> + ⟦ A ⟧ i ;; I ↘ PA -> + ⟦ A ⟧ i ;; I' ↘ PA. +Proof. + move => hI h. + elim : A PA /h. + - hauto lq:on rew:off ctrs:InterpExt. + - hauto q:on ctrs:InterpExt. + - hauto lq:on ctrs:InterpExt. +Qed. + +Lemma InterpExt_lt_eq {n : nat} i I I' A (PA : Tm n -> Prop) : + (forall j, j < i -> I n j = I' n j) -> + ⟦ A ⟧ i ;; I ↘ PA = + ⟦ A ⟧ i ;; I' ↘ PA. +Proof. + move => hI. apply propositional_extensionality. + have : forall j, j < i -> I' n j = I n j by sfirstorder. + firstorder using InterpExt_lt_impl. +Qed. + +Notation "⟦ A ⟧ i ↘ S" := (InterpUnivN i A S) (at level 70). + +Lemma InterpUnivN_nolt n i : + @InterpUnivN n i = @InterpExt n i (fun n j (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA). +Proof. + simp InterpUnivN. + extensionality A. extensionality PA. + set I0 := (fun _ => _). + set I1 := (fun _ => _). + apply InterpExt_lt_eq. + hauto q:on. +Qed. + +#[export]Hint Rewrite @InterpUnivN_nolt : InterpUniv. + +Lemma RPar_substone n (a b : Tm (S n)) (c : Tm n): + RPar.R a b -> RPar.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b). + Proof. hauto l:on inv:option use:RPar.substing, RPar.refl. Qed. + +Lemma InterpExt_Fun_inv n i I (A : Tm n) B P + (h : ⟦ Pi A B ⟧ i ;; I ↘ P) : + exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop), + ⟦ A ⟧ i ;; I ↘ PA /\ + (forall a, PA a -> exists PB, PF a PB) /\ + (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\ + P = ProdSpace PA PF. +Proof. + move E : (Pi A B) h => T h. + move : A B E. + elim : T P / h => //. + - hauto l:on. + - move => A A0 PA hA hA0 hPi A1 B ?. subst. + elim /RPar.inv : hA => //= _ A2 A3 B0 B1 hA1 hB0 [*]. subst. + hauto lq:on ctrs:InterpExt use:RPar_substone. +Qed. + +Lemma InterpExt_Fun_nopf n i I (A : Tm n) B PA : + ⟦ A ⟧ i ;; I ↘ PA -> + (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) -> + ⟦ Pi A B ⟧ i ;; I ↘ (ProdSpace PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB)). +Proof. + move => h0 h1. apply InterpExt_Fun =>//. +Qed. + +Lemma InterpUnivN_Fun_nopf n i (A : Tm n) B PA : + ⟦ A ⟧ i ↘ PA -> + (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) -> + ⟦ Pi A B ⟧ i ↘ (ProdSpace PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB)). +Proof. + hauto l:on use:InterpExt_Fun_nopf rew:db:InterpUniv. +Qed. + +Lemma InterpExt_cumulative n i j I (A : Tm n) PA : + i < j -> + ⟦ A ⟧ i ;; I ↘ PA -> + ⟦ A ⟧ j ;; I ↘ PA. +Proof. + move => h h0. + elim : A PA /h0; + hauto l:on ctrs:InterpExt use:PeanoNat.Nat.lt_trans. +Qed. + +Lemma InterpUnivN_cumulative n i (A : Tm n) PA : + ⟦ A ⟧ i ↘ PA -> forall j, i < j -> + ⟦ A ⟧ j ↘ PA. +Proof. + hauto l:on rew:db:InterpUniv use:InterpExt_cumulative. +Qed. + +Lemma InterpExt_preservation n i I (A : Tm n) B P (h : InterpExt i I A P) : + RPar.R A B -> + ⟦ B ⟧ i ;; I ↘ P. +Proof. + move : B. + elim : A P / h; auto. + - move => A B PA PF hPA ihPA hPB hPB' ihPB T hT. + elim /RPar.inv : hT => //. + move => hPar A0 A1 B0 B1 h0 h1 [? ?] ?; subst. + apply InterpExt_Fun; auto. + move => a PB hPB0. + apply : ihPB; eauto. + sfirstorder use:RPar.cong, RPar.refl. + - hauto lq:on inv:RPar.R ctrs:InterpExt. + - move => A B P h0 h1 ih1 C hC. + have [D [h2 h3]] := RPar_diamond _ _ _ _ h0 hC. + hauto lq:on ctrs:InterpExt. +Qed. + +Lemma InterpUnivN_preservation n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) : + RPar.R A B -> + ⟦ B ⟧ i ↘ P. +Proof. hauto l:on rew:db:InterpUnivN use: InterpExt_preservation. Qed. + +Lemma InterpExt_back_preservation_star n i I (A : Tm n) B P (h : ⟦ B ⟧ i ;; I ↘ P) : + rtc RPar.R A B -> + ⟦ A ⟧ i ;; I ↘ P. +Proof. induction 1; hauto l:on ctrs:InterpExt. Qed. + +Lemma InterpExt_preservation_star n i I (A : Tm n) B P (h : ⟦ A ⟧ i ;; I ↘ P) : + rtc RPar.R A B -> + ⟦ B ⟧ i ;; I ↘ P. +Proof. induction 1; hauto l:on use:InterpExt_preservation. Qed. + +Lemma InterpUnivN_preservation_star n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) : + rtc RPar.R A B -> + ⟦ B ⟧ i ↘ P. +Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_preservation_star. Qed. + +Lemma InterpUnivN_back_preservation_star n i (A : Tm n) B P (h : ⟦ B ⟧ i ↘ P) : + rtc RPar.R A B -> + ⟦ A ⟧ i ↘ P. +Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_back_preservation_star. Qed.