Require Export PropL.

(*** Proof Terms with de Bruijn levels/alpha-standardized names. ***)
Inductive pf : Type :=
| PVar : nat → pf
| Lam : nat → form → pf → pf
| Ap : pf → pf → pf
| Expl : pf → form → pf.

Section Assum.
  Variable F : Type.
  Implicit Types A : list F.

Inductive assum (s : F) (n : nat) : list F → Prop :=
  | assumB A : n = |A| → assum s n (s::A)
  | assumS t A : assum s n A → assum s n (t::A).

Lemma in_assum s A :
  s el A ↔ ∃ n, assum s n A.

Lemma assum_inv s n A :
  assum s n A →
  match A with
  | (t::A) ⇒ s = t ∧ n = |A| ∨ assum s n A ∧ n < |A|
  | nil ⇒ False
  end.

Lemma assum_uniq s t n A :
 assum s n A → assum t n A → s = t.

Lemma assum_sig n A :
 {s | assum s n A} + {∀ s, ¬ assum s n A}.
End Assum.

Inductive ndp (A : context) : pf → form → Prop :=
| ndpA n s : assum s n A → ndp A (PVar n) s
| ndpII n d s t : n = |A| → ndp (s::A) d t → ndp A (Lam n s d) (Imp s t)
| ndpIE d e s t : ndp A d (Imp s t) → ndp A e s → ndp A (Ap d e) t
| ndpE d s : ndp A d Fal → ndp A (Expl d s) s.

Lemma nd_ndp A s :
 nd A s ↔ ∃ d, ndp A d s.

(*** Example ***)
Goal ∀ A s t, {d | ndp A d (Imp s (Imp (Not s) t))}.

(*** Inversion Lemma ***)
Lemma ndp_inv A d s :
  ndp A d s →
  match d with
  | PVar x ⇒ assum s x A
  | Lam x t d ⇒
    match s with
    | Imp s1 s2 ⇒ x = |A| ∧ s1 = t ∧ ndp (t::A) d s2
    | _ ⇒ False
    end
  | Ap d e ⇒ ∃ t, ndp A d (Imp t s) ∧ ndp A e t
  | Expl d t ⇒ t = s ∧ ndp A d Fal
  end.

(*** Unique typing ***)
Lemma ndp_uniq_typ A d s t :
 ndp A d s → ndp A d t → s = t.

Goal ∀ A d x, ndp A d (Var x) → ¬ ndp A d Fal.

Goal ∀ A d e s1 t1 u1 s2 t2,
 ndp A d (Imp s1 t1) → ndp A e u1 →
 ndp A d (Imp s2 t2) → ndp A e s2 → s1 = u1.

(*** Decidability of Type Synthesis ***)
Lemma ndp_synth A d :
 {s | ndp A d s} + {¬ ∃ s, ndp A d s}.

(*** Decidability of Type Checking (a direct induction on d fails because of Ap) ***)
Goal ∀ A d s, dec (ndp A d s).

(*** Classical Proof Terms ***)

Inductive pfc : Type :=
| PVarc : nat → pfc
| Lamc : nat → form → pfc → pfc
| Apc : pfc → pfc → pfc
| Contrac : nat → form → pfc → pfc.

Inductive ndcp (A : context) : pfc → form → Prop :=
| ndcpA n s : assum s n A → ndcp A (PVarc n) s
| ndcpII n d s t : n = |A| → ndcp (s::A) d t → ndcp A (Lamc n s d) (Imp s t)
| ndcpIE d e s t : ndcp A d (Imp s t) → ndcp A e s → ndcp A (Apc d e) t
| ndcpC d s n : n = |A| → ndcp (Not s::A) d Fal → ndcp A (Contrac n s d) s.