291 lines
7.6 KiB
Coq
291 lines
7.6 KiB
Coq
Require Import Autosubst2.syntax
|
||
Autosubst2.core Autosubst2.unscoped typing ssreflect List ssrbool.
|
||
|
||
From Hammer Require Import Tactics.
|
||
|
||
Section ren.
|
||
|
||
Variables (T : Set).
|
||
|
||
Definition ren_ok (ξ : nat -> nat) (Γ Δ : list T) :=
|
||
forall i A, lookup i Δ A -> lookup (ξ i) Γ A.
|
||
|
||
Lemma ren_comp ξ ψ (Γ Δ : list T) Ξ :
|
||
ren_ok ξ Γ Δ ->
|
||
ren_ok ψ Δ Ξ ->
|
||
ren_ok (funcomp ξ ψ) Γ Ξ.
|
||
Proof using. sfirstorder unfold:ren_ok. Qed.
|
||
|
||
Lemma ren_shift (A : T) Γ :
|
||
ren_ok S (A :: Γ) Γ.
|
||
Proof using. hauto lq:on ctrs:lookup inv:lookup unfold:ren_ok. Qed.
|
||
|
||
Lemma ren_ext i ξ Γ Δ (A : T) :
|
||
ren_ok ξ Γ Δ ->
|
||
lookup i Γ A ->
|
||
ren_ok (scons i ξ) Γ (A :: Δ).
|
||
Proof using. qauto l:on unfold:ren_ok inv:lookup. Qed.
|
||
|
||
Lemma ren_up ξ (A : T) Γ Δ :
|
||
ren_ok ξ Γ Δ ->
|
||
ren_ok (upRen_Tm_Tm ξ) (A :: Γ) (A :: Δ).
|
||
Proof using.
|
||
rewrite /upRen_Tm_Tm.
|
||
move => h. apply ren_ext. apply : ren_comp; eauto. apply ren_shift.
|
||
apply here.
|
||
Qed.
|
||
|
||
End ren.
|
||
|
||
Arguments ren_ok {T}.
|
||
|
||
Definition bool_leb a b :=
|
||
match a,b with
|
||
| true, false => false
|
||
| _,_ => true
|
||
end.
|
||
|
||
Lemma bool_leb_refl a : bool_leb a a.
|
||
Proof. case : a => //=. Qed.
|
||
|
||
Lemma bool_le_spec a b : Bool.reflect (Bool.le a b) (bool_leb a b).
|
||
Proof. hauto l:on inv:bool ctrs:Bool.reflect. Qed.
|
||
|
||
Module Liftable.
|
||
Lemma lookup_fixed i Γ ℓ A :
|
||
lookup i Γ (ℓ, A) ->
|
||
lookup i (fixed_ctx Γ) (squash ℓ).
|
||
Proof.
|
||
elim : Γ i ℓ A => //=.
|
||
- hauto lq:on inv:lookup.
|
||
- hauto lq:on inv:lookup ctrs:lookup.
|
||
Qed.
|
||
|
||
Lemma lookup_fixed' i Γ ℓ :
|
||
lookup i (fixed_ctx Γ) ℓ ->
|
||
exists A ℓ0, squash ℓ0 = ℓ /\ lookup i Γ (ℓ0, A).
|
||
Proof.
|
||
elim : Γ i ℓ => //=.
|
||
- hauto lq:on inv:lookup.
|
||
- hauto lq:on inv:lookup ctrs:lookup.
|
||
Qed.
|
||
|
||
Lemma fixed_ren_ok ξ Γ Δ :
|
||
ren_ok ξ Γ Δ ->
|
||
ren_ok ξ (fixed_ctx Γ) (fixed_ctx Δ).
|
||
Proof.
|
||
rewrite /ren_ok.
|
||
move => h i ℓ / lookup_fixed' [A][ℓ0][?]hi. subst.
|
||
apply : lookup_fixed; eauto.
|
||
Qed.
|
||
|
||
Lemma renaming ξ Φ Ψ a :
|
||
liftable Ψ a ->
|
||
ren_ok ξ Φ Ψ ->
|
||
liftable Φ (ren_Tm ξ a).
|
||
Proof.
|
||
elim : a ξ Φ Ψ => //=; hauto l:on use:ren_up unfold:ren_ok.
|
||
Qed.
|
||
|
||
Fixpoint ctx_leq Φ Ψ :=
|
||
match Φ, Ψ with
|
||
| nil, nil => true
|
||
| ℓ::Φ, ℓ'::Ψ => bool_leb ℓ ℓ' && ctx_leq Φ Ψ
|
||
| _, _ => false
|
||
end.
|
||
|
||
Lemma ctx_leq_lookup Φ Ψ i ℓ1 :
|
||
ctx_leq Φ Ψ ->
|
||
lookup i Ψ ℓ1 ->
|
||
exists ℓ0, lookup i Φ ℓ0 /\
|
||
Bool.le ℓ0 ℓ1.
|
||
Proof.
|
||
move => + h. move : Φ.
|
||
elim : i Ψ ℓ1 / h.
|
||
- move => A Γ Ψ h.
|
||
case : Ψ h => //=.
|
||
move => B Ψ.
|
||
case : bool_le_spec => //=.
|
||
sfirstorder ctrs:lookup.
|
||
- move => i Γ A B hi ihi Ψ.
|
||
case : Ψ => //=.
|
||
move => C Ψ.
|
||
case : bool_le_spec => //=.
|
||
hauto lq:on ctrs:lookup.
|
||
Qed.
|
||
|
||
Lemma narrowing Φ Ψ a :
|
||
ctx_leq Φ Ψ ->
|
||
liftable Ψ a ->
|
||
liftable Φ a.
|
||
Proof.
|
||
elim : a Φ Ψ => //=.
|
||
- move => n Φ Ψ.
|
||
move : ctx_leq_lookup; repeat move/[apply].
|
||
move => [ℓ1 [h0 h1]].
|
||
suff : ℓ1 = false by congruence.
|
||
hauto q:on inv:bool.
|
||
- sfirstorder.
|
||
- sfirstorder.
|
||
- sfirstorder.
|
||
Qed.
|
||
|
||
End Liftable.
|
||
|
||
|
||
Definition lvl_leb a b :=
|
||
match a, b with
|
||
| Fixed ℓ0, Fixed ℓ1 => Bool.eqb ℓ0 ℓ1
|
||
| Floating ℓ0, Floating ℓ1 => bool_leb ℓ0 ℓ1
|
||
| _,_ => false
|
||
end.
|
||
|
||
Lemma lvl_leb_refl a : lvl_leb a a.
|
||
Proof. destruct a,b; sfirstorder use:Bool.eqb_reflx, bool_leb_refl. Qed.
|
||
|
||
Module Typing.
|
||
|
||
Inductive ctx_fleq : list bool -> ctx -> ctx -> Prop :=
|
||
| FL_Nil : ctx_fleq nil nil nil
|
||
| FL_ConsFixed Φ Γ Δ A :
|
||
ctx_fleq Φ Γ Δ ->
|
||
ctx_fleq (false :: Φ) (A :: Γ) (A :: Δ)
|
||
| FL_ConsFloat Φ Γ Δ ℓ0 ℓ1 A :
|
||
ctx_fleq Φ Γ Δ ->
|
||
lvl_leb ℓ0 ℓ1 ->
|
||
ctx_fleq (true :: Φ) ((ℓ0, A) :: Γ) ((ℓ1, A) :: Δ).
|
||
|
||
Lemma ctx_fleq_fixed Φ Γ Δ :
|
||
ctx_fleq Φ Γ Δ ->
|
||
ctx_fleq (fixed_ctx Γ) Γ Δ.
|
||
Proof.
|
||
move => h. elim : Φ Γ Δ/ h => //=.
|
||
- constructor.
|
||
- move => Φ Γ Δ [ℓ B].
|
||
move => h0 h1.
|
||
destruct ℓ => //=; constructor; eauto using lvl_leb_refl.
|
||
- move => Φ Γ Δ ℓ0 ℓ1 A hctx ihctx h0.
|
||
destruct ℓ0, ℓ1 => //=.
|
||
simpl in h0.
|
||
move : h0. case : Bool.eqb_spec => //= ? _. subst.
|
||
by constructor.
|
||
by constructor.
|
||
Qed.
|
||
|
||
Lemma renaming ξ Γ Δ ℓ a A :
|
||
Δ ⊢ a ;; ℓ ∈ A ->
|
||
ren_ok ξ Γ Δ ->
|
||
Γ ⊢ ren_Tm ξ a ;; ℓ ∈ A.
|
||
Proof.
|
||
move => h. move : ξ Γ.
|
||
elim : Δ a ℓ A / h.
|
||
- hauto lq:on ctrs:Wt unfold:ren_ok.
|
||
- hauto lq:on ctrs:Wt unfold:ren_ok.
|
||
- hauto lq:on ctrs:Wt use:ren_up.
|
||
- move => Γ ℓ ℓ0 a b A B hb ihb ha iha hl ξ Δ hξ.
|
||
have ? : liftable (fixed_ctx Δ) (ren_Tm ξ a) by
|
||
qauto l:on use:Liftable.renaming, Liftable.fixed_ren_ok.
|
||
hauto lq:on ctrs:Wt.
|
||
- hauto lq:on ctrs:Wt use:ren_up.
|
||
Qed.
|
||
|
||
Lemma ctx_fleq_lookup i Φ (Γ Δ : ctx) A :
|
||
ctx_fleq Φ Γ Δ ->
|
||
lookup i Φ false ->
|
||
lookup i Γ A ->
|
||
lookup i Δ A.
|
||
Proof.
|
||
move => h. move : A i.
|
||
elim : Φ Γ Δ / h => //=; sauto.
|
||
Qed.
|
||
|
||
Lemma ctx_fleq_fixed_eq Φ Γ Δ :
|
||
ctx_fleq Φ Γ Δ ->
|
||
fixed_ctx Γ = fixed_ctx Δ.
|
||
Proof.
|
||
move => h. elim : Φ Γ Δ / h => //=.
|
||
- hauto lq:on.
|
||
- move => Φ Γ Δ ℓ0 ℓ1 h ih h0 h1.
|
||
f_equal => //.
|
||
move {h0 ih h}.
|
||
hauto lq:on inv:Level.
|
||
Qed.
|
||
|
||
Lemma upgrading_liftable Φ Γ Δ a ℓ A :
|
||
Γ ⊢ a ;; ℓ ∈ A ->
|
||
liftable Φ a ->
|
||
ctx_fleq Φ Γ Δ ->
|
||
Δ ⊢ a ;; ℓ ∈ A.
|
||
Proof.
|
||
move => h. move : Φ Δ.
|
||
elim : Γ a ℓ A /h.
|
||
- move => Γ ℓ i ℓ0 A hℓ hi Φ Δ /= h0 h1.
|
||
econstructor; eauto.
|
||
eauto using ctx_fleq_lookup.
|
||
- hauto lq:on ctrs:Wt.
|
||
- move => Γ ℓ a A B ha iha Φ Δ hla hleq /=.
|
||
constructor. apply : iha => /=; cycle 1; eauto.
|
||
by constructor.
|
||
- move => Γ ℓ ℓ0 a b A B hb ihb ha iha hla Φ Δ /= hlb hctx.
|
||
apply : T_App; eauto.
|
||
apply : iha; eauto.
|
||
sfirstorder use:ctx_fleq_fixed.
|
||
erewrite <- ctx_fleq_fixed_eq; eauto.
|
||
- move => Γ ℓ ℓ0 b A B hb ihb Δ /=.
|
||
move => h0 h1. constructor. apply : ihb; eauto.
|
||
simpl. by constructor.
|
||
Qed.
|
||
|
||
Definition or_lvl (a : bool) l :=
|
||
match l with
|
||
| Fixed ℓ => Fixed ℓ
|
||
| Floating ℓ => Floating (a || ℓ)
|
||
end.
|
||
|
||
Definition or_ctx (a : bool) : ctx -> ctx := map (fun '(ℓ,A) => (or_lvl a ℓ, A)).
|
||
|
||
Lemma or_fixed_ctx ℓ (Γ : ctx) :
|
||
fixed_ctx (or_ctx ℓ Γ) = fixed_ctx Γ.
|
||
Proof.
|
||
elim : Γ => //=.
|
||
- case => //=.
|
||
move => ℓ0 _ Γ.
|
||
move => h0. f_equal => //.
|
||
destruct ℓ0 => //=.
|
||
Qed.
|
||
|
||
Definition or_ctx_lookup ℓ0 i Γ ℓ A :
|
||
lookup i Γ (ℓ, A) ->
|
||
lookup i (or_ctx ℓ0 Γ) (or_lvl ℓ0 ℓ, A).
|
||
Proof.
|
||
elim : Γ i ℓ A; sauto.
|
||
Qed.
|
||
|
||
Lemma upgrading Γ a ℓ A :
|
||
Γ ⊢ a ;; ℓ ∈ A ->
|
||
or_ctx ℓ Γ ⊢ a ;; ℓ ∈ A.
|
||
Proof.
|
||
move => h. elim : Γ a ℓ A /h.
|
||
- move => Γ ℓ i ℓ0 A hℓ hi.
|
||
move /(or_ctx_lookup ℓ) in hi.
|
||
apply T_Var with (ℓ0 := or_lvl ℓ ℓ0); eauto.
|
||
destruct ℓ0, ℓ => //=.
|
||
- hauto lq:on ctrs:Wt.
|
||
- move => Γ ℓ a A B /= ha iha.
|
||
rewrite Bool.orb_diag in iha.
|
||
hauto lq:on ctrs:Wt.
|
||
- move => Γ ℓ ℓ0 a b A B hb ihb ha iha hla.
|
||
econstructor; eauto.
|
||
+ apply : upgrading_liftable. apply ha. eauto. clear.
|
||
elim : Γ => //=.
|
||
* constructor.
|
||
* case => //= ℓ0 A Γ h0.
|
||
destruct ℓ0 => //=.
|
||
by constructor.
|
||
constructor => //.
|
||
clear. sauto lq:on.
|
||
+ by rewrite or_fixed_ctx.
|
||
- hauto lq:on ctrs:Wt.
|
||
Qed.
|
||
|
||
End Typing.
|