Library Weakening

Weakening

Require Export Types.
Implicit Types x y z : var.
Implicit Types F G H : basetype.
Implicit Types A B C : inttype.
Implicit Types U V W : type.
Implicit Types Gamma Delta : context.

A parallel renaming from Gamma to Delta is an invertible function that maps the variables in Gamma to variables in Delta such that they agree on the types

Inductive tyren xi Gamma Delta : Prop :=
| tyrenInv (ceta : var -> option var) :
(forall v x, ceta v = Some x -> xi x = v) ->
(forall x, ceta (xi x) = Some x) -> (forall x, Gamma x = Delta (xi x)) -> tyren xi Gamma Delta.

Hint Constructors tyren.

Increments the variable if there is one

Definition inc ox := match ox with None => None | Some x => Some (S x) end.

Extending with the identity mapping does not break renamings

Lemma tyren_up {xi Gamma Delta} : tyren xi Gamma Delta ->
  forall U,
    tyren (0 .: xi >>> (+1)) (U .: Gamma) (U .: Delta).
intros [ceta Bi1 Bi2 T] U.
exists (fun x => match x with 0 => Some 0 | S x' => inc (ceta x') end).
- intros [|v] [|x] H ; simpl in * ; try congruence.
  + destruct (ceta v) ; discriminate.
  + f_equal. apply Bi1. destruct (ceta v) ; simpl in * ; congruence.
- intros [|x] ; simpl ; auto.
  now rewrite Bi2.
- intros [|x] ; simpl ; auto.
Qed.

Typing of variables is stable under renaming

Lemma tyren_var {xi Gamma Delta} : tyren xi Gamma Delta -> forall n x U, Gamma x >= U ->
ty n Delta (xi x) U.
intros [ceta Bi1 Bi2 T] n x U le.
rewrite (T x) in le.
now apply tyVarU.
Qed.

Renamings that translate from the intersection of Gamma1 and Gamma2 to Delta can be split into renamings that translate from Gamma1 to Delta1 and Gamma2 to Delta2, such that Delta1 & Delta2 is point wise equivalent to Delta

Lemma tyren_split {xi Gamma Delta} : tyren xi Gamma Delta -> forall {Gamma1 Gamma2}, Gamma1 & Gamma2 ==1 Gamma -> exists Delta1 Delta2, tyren xi Gamma1 Delta1 /\ tyren xi Gamma2 Delta2 /\ Delta ==1 Delta1 & Delta2.
intros [ceta Bi1 Bi2 T] Gamma1 Gamma2 E'.
exists (fun x => match ceta x with None => OMEGA | Some y => Gamma1 y end),
       (fun x => match ceta x with None => Delta x | Some y => Gamma2 y end).
intuition.
- econstructor ; eauto. intros x. now rewrite Bi2.
- econstructor ; eauto. intros x. now rewrite Bi2.
- intros x ; simpl.
  remember (ceta x) as y ; destruct y ; auto.
  rewrite (E' v), T.
  rewrite (Bi1 x v) ; eauto.
Qed.

Typing is stable under renaming

Theorem weaken n Gamma s U : ty n Gamma s U -> forall xi Delta, tyren xi Gamma Delta ->
  ty n Delta s .[ren (xi)] U.
induction 1 ; intros xi Gamma' tr ; simpl ; subst ; eauto using tyren_var.
- constructor. asimpl. auto using tyren_up.
- destruct (tyren_split tr e) as [Delta1 [Delta2 [tr1 [tr2 E]]]].
  eauto.
- destruct (tyren_split tr e) as [Delta1 [Delta2 [tr1 [tr2 E]]]].
  eauto.
Qed.

Typing is monotone in the context

Corollary weakening n Gamma s U : ty n Gamma s U -> forall V, ty n (V .: Gamma) s .[ren (+1)] U.
intros T V.
eapply weaken ; eauto.
exists (fun x => match x with 0 => None | S x' => Some x' end) ; eauto.
intros [|v] x E ; simpl ; congruence.
Qed.

Hint Resolve weakening.