working on completeness rules for subtyping

theories/Core/Completeness/ContextCases.v

@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases.
+From Mcltt.Core Require Import Evaluation Completeness.LogicalRelation Completeness.UniverseCases.
 Import Domain_Notations.
 
 Proposition valid_ctx_empty :
@@ -41,5 +41,37 @@ Proof with intuition.
   - apply Equivalence_Reflexive.
 Qed.
 
+Lemma rel_ctx_extend' : forall {Γ A i},
+    {{ Γ ⊨ A : Type@i }} ->
+    {{ ⊨ Γ, A }}.
+Proof.
+  intros.
+  eapply rel_ctx_extend; eauto.
+  destruct H as [? []].
+  eexists. eassumption.
+Qed.
+
 #[export]
-Hint Resolve rel_ctx_extend : mcltt.
+Hint Resolve rel_ctx_extend rel_ctx_extend' : mcltt.
+
+
+Lemma wf_ctx_sub_empty' :
+  {{ SubE ⋅ <: ⋅ }}.
+Proof. mauto. Qed.
+
+
+Lemma wf_ctx_sub_extend' : forall Γ Δ i A A',
+  {{ SubE Γ <: Δ }} ->
+  {{ Γ ⊨ A : Type@i }} ->
+  {{ Δ ⊨ A' : Type@i }} ->
+  {{ Γ ⊨ A ⊆ A' }} ->
+  {{ SubE Γ , A <: Δ , A' }}.
+Proof.
+  intros * H H1 H2 H3.
+  pose proof H3.
+  destruct H3 as [? [? []]].
+  on_all_hyp: fun H => (eapply rel_ctx_extend' in H; destruct H).
+  econstructor; mauto; intros.
+  deepexec H3 ltac:(fun H => destruct H as []).
+  simplify_evals. eassumption.
+Qed.

theories/Core/Completeness/LogicalRelation/Definitions.v

@@ -45,9 +45,15 @@ Hint Transparent valid_sub_under_ctx : mcltt.
 #[export]
 Hint Unfold valid_sub_under_ctx : mcltt.
 
+Definition sub_typ_under_ctx Γ M M' :=
+  exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
+  forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+    rel_exp M p M' p' (per_subtyp i).
+
 Notation "⊨ Γ ≈ Γ'" := (per_ctx Γ Γ')  (in custom judg at level 80, Γ custom exp, Γ' custom exp).
 Notation "⊨ Γ" := (valid_ctx Γ) (in custom judg at level 80, Γ custom exp).
 Notation "Γ ⊨ M ≈ M' : A" := (rel_exp_under_ctx Γ A M M') (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
+Notation "Γ ⊨ M ⊆ M'" := (sub_typ_under_ctx Γ M M') (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp).
 Notation "Γ ⊨ M : A" := (valid_exp_under_ctx Γ A M) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
 Notation "Γ ⊨s σ ≈ σ' : Δ" := (rel_sub_under_ctx Γ Δ σ σ') (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
 Notation "Γ ⊨s σ : Δ" := (valid_sub_under_ctx Γ Δ σ) (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).

theories/Core/Semantic/PER/Lemmas.v

@@ -628,46 +628,6 @@ Proof.
 Qed.
 
 
-Lemma PER_refl1 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R a a.
-Proof.
-  intros.
-  etransitivity; [eassumption |].
-  symmetry. assumption.
-Qed.
-
-Lemma PER_refl2 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R b b.
-Proof.
-  intros. symmetry in H.
-  apply PER_refl1 in H;
-    auto.
-Qed.
-
-Ltac saturate_refl :=
-  repeat match goal with
-    | H : ?R ?a ?b |- _ =>
-        tryif unify a b
-        then fail
-        else
-          directed pose proof (PER_refl1 _ _ _ _ _ H);
-        directed pose proof (PER_refl2 _ _ _ _ _ H);
-        fail_if_dup
-    end.
-
-Ltac saturate_refl_for hd :=
-  repeat match goal with
-    | H : ?R ?a ?b |- _ =>
-        unify R hd;
-        tryif unify a b
-        then fail
-        else
-          directed pose proof (PER_refl1 _ _ _ _ _ H);
-        directed pose proof (PER_refl2 _ _ _ _ _ H);
-        fail_if_dup
-    end.
-
-Ltac solve_refl :=
-  solve [reflexivity || apply Equivalence_Reflexive].
-
 Lemma per_elem_subtyping : forall A B i,
     {{ Sub A <: B at i }} ->
     forall R R' a b,

theories/LibTactics.v

@@ -1,4 +1,4 @@
-From Coq Require Export Program.Equality Program.Tactics Lia RelationClasses.
+From Coq Require Export Relations.Relation_Definitions Program.Equality Program.Tactics Lia RelationClasses.
 
 Open Scope predicate_scope.
 
@@ -354,3 +354,47 @@ Ltac unify_args H P :=
     | H : Symmetric _ |- _ => clear H
     | H : Transitive _ |- _ => clear H
     end.
+
+
+Lemma PER_refl1 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R a a.
+Proof.
+  intros.
+  etransitivity; [eassumption |].
+  symmetry. assumption.
+Qed.
+
+Lemma PER_refl2 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R b b.
+Proof.
+  intros. symmetry in H.
+  apply PER_refl1 in H;
+    auto.
+Qed.
+
+#[global]
+  Ltac saturate_refl :=
+  repeat match goal with
+    | H : ?R ?a ?b |- _ =>
+        tryif unify a b
+        then fail
+        else
+          directed pose proof (PER_refl1 _ _ _ _ _ H);
+        directed pose proof (PER_refl2 _ _ _ _ _ H);
+        fail_if_dup
+    end.
+
+#[global]
+  Ltac saturate_refl_for hd :=
+  repeat match goal with
+    | H : ?R ?a ?b |- _ =>
+        unify R hd;
+        tryif unify a b
+        then fail
+        else
+          directed pose proof (PER_refl1 _ _ _ _ _ H);
+        directed pose proof (PER_refl2 _ _ _ _ _ H);
+        fail_if_dup
+    end.
+
+#[global]
+  Ltac solve_refl :=
+  solve [reflexivity || apply Equivalence_Reflexive].