oadt.lang_oadt.inversion

Typing and kinding inversion lemmas.
From oadt Require Import lang_oadt.base.
From oadt Require Import lang_oadt.syntax.
From oadt Require Import lang_oadt.semantics.
From oadt Require Import lang_oadt.typing.
From oadt Require Import lang_oadt.infrastructure.
From oadt Require Import lang_oadt.equivalence.

Import syntax.notations.
Import semantics.notations.
Import typing.notations.

Implicit Types (b : ) (x X y Y : atom) (L : aset).

#[local]
Coercion EFVar : atom >-> expr.

Section inversion.

Context (Σ : gctx).
Context (Hwf : gctx_wf Σ).

#[local]
Set Default Proof Using "Type".

Kind inversion

Tactic Notation "kind_inv_solver" "by" (tac) :=
  match goal with
  | |- _; _ :: _ -> _ => remember τ
  end;
  induction 1; subst; simp_hyps; simplify_eq;
  tac.

Tactic Notation "kind_inv_solver" :=
  kind_inv_solver by (repeat esplit; eauto; lattice_naive_solver).

Lemma kind_inv_pi Γ κ :
  Σ; Γ Π:, :: κ ->
  κ = <{ *@M }>
   L ,
    ( x, x L Σ; (<[x:=]> Γ) ^x :: )
    Σ; Γ :: .
Proof.
  kind_inv_solver by sfirstorder use: top_inv.
Qed.


Lemma kind_inv_bool Γ κ :
  Σ; Γ 𝔹 :: κ -> <{ *@P }> κ.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_prod Γ κ :
  Σ; Γ * :: κ ->
   κ',
    Σ; Γ :: κ'
    Σ; Γ :: κ'
    <{ κ' }> κ.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_sum Γ κ :
  Σ; Γ + :: κ ->
  <{ *@P }> κ
   κ',
    Σ; Γ :: κ'
    Σ; Γ :: κ'.
Proof.
  kind_inv_solver by qauto l: on use: join_ub_r
                           solve: lattice_naive_solver.
Qed.


Lemma kind_inv_osum Γ κ :
  Σ; Γ ~+ :: κ ->
  <{ *@O }> κ
  Σ; Γ :: *@O
  Σ; Γ :: *@O.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_gvar Γ X κ :
  Σ; Γ gvar X :: κ ->
  <{ *@P }> κ τ, Σ !! X = Some (DADT τ).
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_app Γ κ :
  Σ; Γ :: κ ->
  <{ *@O }> κ
   X τ e',
    Σ !! X = Some (DOADT τ e')
    Σ; Γ : τ
     = <{ gvar X }>.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_ite Γ l κ :
  Σ; Γ if{l} then else :: κ ->
  <{ *@O }> κ
  l = low
  Σ; Γ : 𝔹
  Σ; Γ :: *@O
  Σ; Γ :: *@O.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_let Γ e τ κ :
  Σ; Γ let e in τ :: κ ->
  <{ *@O }> κ
   τ' L,
    Σ; Γ e : τ'
    ( x, x L -> Σ; (<[x:=τ']> Γ) τ^x :: *@O).
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_case Γ l κ :
  Σ; Γ case{l} of | :: κ ->
  <{ *@O }> κ
  l = low
   ,
    Σ; Γ : +
    ( x, x -> Σ; (<[x:=]> Γ) ^x :: *@O)
    ( x, x -> Σ; (<[x:=]> Γ) ^x :: *@O).
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_mux Γ κ :
  Σ; Γ ~if then else :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_sec Γ e κ :
  Σ; Γ s𝔹 e :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_pair Γ κ :
  Σ; Γ (, ) :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_proj Γ b e κ :
  Σ; Γ π@b e :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_inj Γ l b τ e κ :
  Σ; Γ inj{l}@b<τ> e :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_ocase Γ κ :
  Σ; Γ ~case of | :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_fold Γ X e κ :
  Σ; Γ fold<X> e :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_unfold Γ X e κ :
  Σ; Γ unfold<X> e :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Lemma kind_inv_abs Γ τ e κ :
  Σ; Γ \:τ => e :: κ -> False.
Proof.
  kind_inv_solver.
Qed.


Type inversion

Tactic Notation "type_inv_solver" "by" (tac) :=
  match goal with
  | |- _; _ ?e : _ -> _ => remember e
  end;
  induction 1; subst; simp_hyps; simplify_eq;
  tac.

Tactic Notation "type_inv_solver" :=
  type_inv_solver by (repeat esplit; eauto; equiv_naive_solver).

Lemma type_inv_prod Γ τ :
  Σ; Γ * : τ -> False.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_sum Γ l τ :
  Σ; Γ +{l} : τ -> False.
Proof.
  type_inv_solver.
Qed.


From now on proofs rely on well-formedness of global context.
#[local]
Set Default Proof Using "Hwf".

Lemma type_inv_unit Γ τ :
  Σ; Γ () : τ ->
  Σ τ 𝟙.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_lit Γ b τ :
  Σ; Γ lit b : τ ->
  Σ τ 𝔹.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_abs Γ e τ :
  Σ; Γ \: => e : τ ->
   κ L,
    Σ; Γ :: κ
    ( x, x L -> Σ; (<[x:=]> Γ) e^x : ^x)
    Σ τ Π:, .
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_gvar Γ x τ :
  Σ; Γ gvar x : τ ->
   τ' e,
    Σ !! x = Some (DFun τ' e)
    Σ τ τ'.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_pair Γ τ :
  Σ; Γ (, ) : τ ->
   ,
    Σ; Γ :
    Σ; Γ :
    Σ τ * .
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_inj Γ b e τ' τ :
  Σ; Γ inj@b<τ'> e : τ ->
   κ,
    τ' = <{ + }>
    Σ; Γ + :: κ
    Σ; Γ e : ite b
    Σ τ + .
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_oinj Γ b e τ' τ :
  Σ; Γ ~inj@b<τ'> e : τ ->
   ,
    τ' = <{ ~+ }>
    Σ; Γ ~+ :: *@O
    Σ; Γ e : ite b
    Σ τ ~+ .
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_fold Γ X e τ :
  Σ; Γ fold<X> e : τ ->
   τ',
    Σ; Γ e : τ'
    Σ !! X = Some (DADT τ')
    Σ τ gvar X.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_boxedlit Γ b τ :
  Σ; Γ [b] : τ ->
  Σ τ ~𝔹.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_boxedinj Γ b v ω τ :
  Σ; Γ [inj@b<ω> v] : τ ->
   ,
    ω = <{ ~+ }>
    ovalty <{ [inj@b<ω> v] }> ω
    Σ τ ~+ .
Proof.
  type_inv_solver by hauto lq: on ctrs: ovalty inv: ovalty
                           solve: equiv_naive_solver.
Qed.


Lemma type_inv_case Γ τ :
  Σ; Γ case of | : τ ->
   τ' κ ,
    Σ; Γ τ'^ :: κ
    Σ; Γ : +
    ( x, x -> Σ; (<[x:=]> Γ) ^x : τ'^(inl< + > x))
    ( x, x -> Σ; (<[x:=]> Γ) ^x : τ'^(inr< + > x))
    Σ τ τ'^.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_ocase Γ τ :
  Σ; Γ ~case of | : τ ->
   τ' ,
    Σ; Γ τ' :: *@O
    Σ; Γ : ~+
    ( x, x -> Σ; (<[x:=]> Γ) ^x : τ')
    ( x, x -> Σ; (<[x:=]> Γ) ^x : τ')
    Σ τ τ'.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_case_ Γ l τ :
  Σ; Γ case{l} of | : τ ->
   τ' κ ,
    Σ; Γ τ' :: κ
    Σ; Γ : +{l}
    ( x, x -> τ', Σ; (<[x:=]> Γ) ^x : τ')
    ( x, x -> τ', Σ; (<[x:=]> Γ) ^x : τ')
    Σ τ τ'.
Proof.
  type_inv_solver by (repeat (esplit; eauto); equiv_naive_solver).
Qed.


Lemma type_inv_app Γ τ :
  Σ; Γ : τ ->
   ,
    Σ; Γ : Π:,
    Σ; Γ :
    Σ τ ^.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_let Γ τ :
  Σ; Γ let in : τ ->
   L,
    Σ; Γ :
    ( x, x L -> Σ; (<[x:=]> Γ) ^x : ^x)
    Σ τ ^.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_sec Γ e τ :
  Σ; Γ s𝔹 e : τ ->
  Σ; Γ e : 𝔹
  Σ τ ~𝔹.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_ite Γ τ :
  Σ; Γ if then else : τ ->
   τ' κ,
    Σ; Γ : 𝔹
    Σ; Γ : τ'^(lit true)
    Σ; Γ : τ'^(lit false)
    Σ; Γ τ'^ :: κ
    Σ τ τ'^.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_mux Γ τ :
  Σ; Γ ~if then else : τ ->
   τ',
    Σ; Γ : ~𝔹
    Σ; Γ : τ'
    Σ; Γ : τ'
    Σ; Γ τ' :: *@O
    Σ τ τ'.
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_proj Γ b e τ :
  Σ; Γ π@b e : τ ->
   ,
    Σ; Γ e : *
    Σ τ ite b .
Proof.
  type_inv_solver.
Qed.


Lemma type_inv_unfold Γ X e τ :
  Σ; Γ unfold<X> e : τ ->
   τ',
    Σ !! X = Some (DADT τ')
    Σ; Γ e : gvar X
    Σ τ τ'.
Proof.
  type_inv_solver.
Qed.


End inversion.

Tactics


Tactic Notation "apply_kind_inv" hyp(H) "by" (tac) :=
  lazymatch type of H with
  | _; _ Π:_, _ :: _ => tac kind_inv_pi
  | _; _ 𝔹 :: _ => tac kind_inv_bool
  | _; _ _ _ :: _ => tac kind_inv_app
  | _; _ let _ in _ :: _ => tac kind_inv_let
  | _; _ _ * _ :: _ => tac kind_inv_prod
  | _; _ _ + _ :: _ => tac kind_inv_sum
  | _; _ _ ~+ _ :: _ => tac kind_inv_osum
  | _; _ gvar _ :: _ => tac kind_inv_gvar
  | _; _ ~if _ then _ else _ :: _ => apply kind_inv_mux in H; elim H
  | _; _ if{_} _ then _ else _ :: _ => tac kind_inv_ite
  | _; _ ~case _ of _ | _ :: _ => apply kind_inv_ocase in H; elim H
  | _; _ case{_} _ of _ | _ :: _ => tac kind_inv_case
  | _; _ s𝔹 _ :: _ => apply kind_inv_sec in H; elim H
  | _; _ (_, _) :: _ => apply kind_inv_pair in H; elim H
  | _; _ π@_ _ :: _ => apply kind_inv_proj in H; elim H
  | _; _ inj{_}@_<_> _ :: _ => apply kind_inv_inj in H; elim H
  | _; _ fold<_> _ :: _ => apply kind_inv_fold in H; elim H
  | _; _ unfold<_> _ :: _ => apply kind_inv_unfold in H; elim H
  | _; _ \:_ => _ :: _ => apply kind_inv_abs in H; elim H
  end.

Tactic Notation "apply_kind_inv" hyp(H) :=
  apply_kind_inv H by ( lem => apply lem in H; try simp_hyp H).

Tactic Notation "apply_kind_inv" :=
  do_hyps ( H => try apply_kind_inv H).

Tactic Notation "apply_kind_inv" "*" :=
  do_hyps ( H => try dup_hyp H ( H => apply_kind_inv H)).

Tactic Notation "apply_type_inv" hyp(H) "by" (tac) :=
  lazymatch type of H with
  | _; _ () : _ => tac type_inv_unit
  | _; _ lit _ : _ => tac type_inv_lit
  | _; _ gvar _ : _ => tac type_inv_gvar
  | _; _ \:_ => _ : _ => tac type_inv_abs
  | _; _ _ _ : _ => tac type_inv_app
  | _; _ let _ in _ : _ => tac type_inv_let
  | _; _ (_, _) : _ => tac type_inv_pair
  | _; _ s𝔹 _ : _ => tac type_inv_sec
  | _; _ π@_ _ : _ => tac type_inv_proj
  | _; _ ~inj@_<_> _ : _ => tac type_inv_oinj
  | _; _ inj@_<_> _ : _ => tac type_inv_inj
  | _; _ ~if _ then _ else _ : _ => tac type_inv_mux
  | _; _ if _ then _ else _ : _ => tac type_inv_ite
  | _; _ ~case _ of _ | _ : _ => tac type_inv_ocase
  | _; _ case _ of _ | _ : _ => tac type_inv_case
  | _; _ case{_} _ of _ | _ : _ => tac type_inv_case_
  | _; _ fold<_> _ : _ => tac type_inv_fold
  | _; _ unfold<_> _ : _ => tac type_inv_unfold
  | _; _ [_] : _ => tac type_inv_boxedlit
  | _; _ [inj@_<_> _] : _ => tac type_inv_boxedinj
  | _; _ _ * _ : _ => apply type_inv_prod in H; elim H
  | _; _ _ +{_} _ : _ => apply type_inv_sum in H; elim H
  end.

Tactic Notation "apply_type_inv" hyp(H) :=
  apply_type_inv H by ( lem => apply lem in H; try simp_hyp H);
  try lazymatch goal with
      | |- gctx_wf _ => assumption
      end.

Tactic Notation "apply_type_inv" :=
  do_hyps ( H => try apply_type_inv H).

Tactic Notation "apply_type_inv" "*" :=
  do_hyps ( H => try dup_hyp H ( H => apply_type_inv H)).