theories/logrel.v

@@ -0,0 +1,140 @@
+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 ssrbool.
+Require Import Logic.PropExtensionality (propositional_extensionality).
+From stdpp Require Import relations (rtc(..), rtc_subrel).
+Import Psatz.
+
+Definition ProdSpace {n} (PA : PTm n -> Prop)
+  (PF : PTm n -> (PTm n -> Prop) -> Prop) b : Prop :=
+  forall a PB, PA a -> PF a PB -> PB (PApp b a).
+
+Definition SumSpace {n} (PA : PTm n -> Prop)
+  (PF : PTm n -> (PTm n -> Prop) -> Prop) t : Prop :=
+  SNe t \/ exists a b, rtc TRedSN t (PPair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
+
+Definition BindSpace {n} p := if p is PPi then @ProdSpace n else SumSpace.
+
+Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70).
+
+Inductive InterpExt {n} i (I : nat -> PTm n -> Prop) : PTm n -> (PTm n -> Prop) -> Prop :=
+| InterpExt_Ne A :
+  SNe A ->
+  ⟦ A ⟧ i ;; I ↘ SNe
+| InterpExt_Bind p A B PA PF :
+  ⟦ A ⟧ i ;; I ↘ PA ->
+  (forall a, PA a -> exists PB, PF a PB) ->
+  (forall a PB, PF a PB -> ⟦ subst_PTm (scons a VarPTm) B ⟧ i ;; I ↘ PB) ->
+  ⟦ PBind p A B ⟧ i ;; I ↘ BindSpace p PA PF
+
+| InterpExt_Univ j :
+  j < i ->
+  ⟦ PUniv j ⟧ i ;; I ↘ (I j)
+
+| InterpExt_Step A A0 PA :
+  TRedSN 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 : PTm n -> Prop) :
+  PF = I j ->
+  j < i ->
+  ⟦ PUniv j ⟧ i ;; I ↘ PF.
+Proof. hauto lq:on ctrs:InterpExt. Qed.
+
+Infix "<?" := Compare_dec.lt_dec (at level 60).
+
+Equations InterpUnivN n (i : nat) : PTm n -> (PTm n -> Prop) -> Prop by wf i lt :=
+  InterpUnivN n i := @InterpExt n i
+                     (fun j A =>
+                        match j <? i  with
+                        | left _ => exists PA, InterpUnivN n j A PA
+                        | right _ => False
+                        end).
+Arguments InterpUnivN {n}.
+
+Lemma InterpExt_lt_impl n i I I' A (PA : PTm n -> Prop) :
+  (forall j, j < i -> I j = I' j) ->
+  ⟦ A ⟧ i ;; I ↘ PA ->
+  ⟦ A ⟧ i ;; I' ↘ PA.
+Proof.
+  move => hI h.
+  elim : A PA /h.
+  - hauto q:on ctrs:InterpExt.
+  - hauto lq:on rew:off ctrs:InterpExt.
+  - hauto q:on ctrs:InterpExt.
+  - hauto lq:on ctrs:InterpExt.
+Qed.
+
+Lemma InterpExt_lt_eq n i I I' A (PA : PTm n -> Prop) :
+  (forall j, j < i -> I j = I' j) ->
+  ⟦ A ⟧ i ;; I ↘ PA =
+  ⟦ A ⟧ i ;; I' ↘ PA.
+Proof.
+  move => hI. apply propositional_extensionality.
+  have : forall j, j < i -> I' j = I 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 j (A : PTm 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.
+
+Derive Dependent Inversion iinv with (forall n i I (A : PTm n) PA, InterpExt i I A PA) Sort Prop.
+
+Lemma InterpExt_cumulative n i j I (A : PTm 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 solve+:(by lia).
+Qed.
+
+Lemma InterpUniv_cumulative n i (A : PTm n) PA :
+   ⟦ A ⟧ i ↘ PA -> forall j, i <= j ->
+   ⟦ A ⟧ j ↘ PA.
+Proof.
+  hauto l:on rew:db:InterpUniv use:InterpExt_cumulative.
+Qed.
+
+Definition CR {n} (P : PTm n -> Prop) :=
+  (forall a, P a -> SN a) /\
+    (forall a, SNe a -> P a).
+
+Lemma adequacy_ext i n I A PA
+  (hI0 : forall j,  j < i -> forall a b, (TRedSN a b) ->  I j b -> I j a)
+  (hI : forall j, j < i -> CR (I j))
+  (h :  ⟦ A : PTm n ⟧ i ;; I ↘ PA) :
+  CR PA /\ SN A.
+Proof.
+  elim : A PA / h.
+  - hauto lq:on ctrs:SN unfold:CR.
+  - move => p A B PA PF hPA [ihA0 ihA1] hTot hRes ihPF.
+    have x : fin n by admit.
+    set Bot := VarPTm x.
+    have hb : PA Bot by hauto q:on ctrs:SNe.
+    rewrite /CR.
+    repeat split.
+    + case : p =>//=.
+      * rewrite /ProdSpace.
+        qauto use:SN_AppInv unfold:CR.
+      * rewrite /SumSpace => a []; first by apply N_SNe.
+        move => [q0][q1]*.
+        have : SN q0 /\ SN q1 by hauto q:on.