Set Implicit Arguments.

Section Kripke.
  
  Variable A : Set.
  
  Inductive prop : Set :=
  | atom : A -> prop
  | impl : prop -> prop -> prop.
  
  Coercion atom : A >-> prop.
  
  Inductive con : Set :=
  | empty : con
  | ext : con -> prop -> con.
  
  Notation " P ==> Q " := (impl P Q) (at level 20).
  
  Notation " C # P " := (ext C P) (at level 30).
  
  Reserved Notation " C |- P " (at level 60).
  
  Inductive vdash : con -> prop -> Prop :=
  | ax : forall C P, C # P |- P
  | weak : forall C P Q, C |- P -> C # Q |- P
  | abs : forall C P Q, C # P |- Q -> C |- P ==> Q
  | app : forall C P Q, C |- P ==> Q -> C |- P -> C |- Q
    
    where " C |- P " := (vdash C P).
  
  Record kripke : Type := mkKripke {
    W : Set ;
    le : W -> W -> Prop;
    id : forall x, le x x;
    trans : forall x y z, le x y -> le y z -> le x z;
    force : W -> A -> Prop;
    mon : forall w w', le w' w -> forall a, force w a -> force w' a
  }.

  (* Definition monotonic U (force : W -> U -> Prop) := forall w w', le w' w -> forall a, force w a -> force w' a. *)

End Kripke.

Notation " P ==> Q " := (impl P Q) (at level 20).
Notation " C # P " := (ext C P) (at level 30).
Notation " C |- P " := (vdash C P) (at level 60).

Section Soundness.

  Variables (A : Set) (K : kripke A).

  Reserved Notation " w ||- P " (at level 60).

  Fixpoint force_prop (w : W K) (p : prop A) {struct p} : Prop :=
  match p with
    | atom a => force K w a
    | impl P Q => forall w', le K w' w -> w' ||- P -> w' ||- Q
  end
  
  where " w ||- P " := (force_prop w P).

  Reserved Notation " w ||-* G " (at level 60).

  Fixpoint force_con (w : W K) (c : con A) {struct c} : Prop :=
    match c with
      | empty => True
      | ext G P => force_con w G /\ w ||- P
    end
    
    where " w ||-* G " := (force_con w G).

  Lemma mon_prop : forall w w', le K w' w -> forall a, force_prop w a -> force_prop w' a.
  Proof.
    induction a.
    intros.
    simpl in H0.
    pose (mon K _ _ H _ H0).
    simpl.
    apply f.

    simpl in *.
    intros.
    apply H0.
    apply trans with w' ; assumption.
    assumption.
  Qed.

  Lemma mon_con : forall w w', le K w' w -> forall a, force_con w a -> force_con w' a.
  Proof with auto.
    induction a.

    simpl ; intros.
    auto.

    simpl ; intros.
    destruct H0.
    split.

    apply IHa ; assumption.
    apply mon_prop with w...
  Qed.

  Lemma soundness : forall C P, C |- P -> forall w, w ||-* C -> w ||- P.
  Proof with auto.
    induction 1 ; simpl ; intros.

    destruct H...

    destruct H0.
    apply IHvdash...

    apply IHvdash.
    simpl.
    split...
    apply mon_con with w...

    simpl in *.
    apply IHvdash1 with w...
    apply id.
  Qed.
End Soundness.

Section Completeness.

  Variable A : Set.

  Reserved Notation " G |-- D " (at level 30).
  Reserved Notation " G |-v t " (at level 30).
  Reserved Notation " G |-ne t " (at level 30).
  Reserved Notation " G |-nf t " (at level 30).

  Inductive vdash_var : con A -> prop A -> Prop :=
  | v_ax : forall C P, (C # P) |-v P
  | v_weak : forall C P Q, (C |-v P) -> (C # Q) |-v P
    
    where " C |-v P " := (vdash_var C P)

  with vdash_ne : con A -> prop A -> Prop :=
  | v2ne : forall C P, C |-v P -> C |-ne P 
  | n_app : forall C P Q, C |-ne (P ==> Q) ->
    (C |-nf P) -> (C |-ne Q)

    where " C |-ne P " := (vdash_ne C P)
    
  with vdash_nf : con A -> prop A -> Prop := 
  | ne2nf : forall C a, (C |-ne a) -> C |-nf a
  | n_abs : forall C P Q, C # P |-nf Q -> C |-nf P ==> Q

    where " C |-nf P " := (vdash_nf C P).
  
  Coercion v2ne : vdash_var >-> vdash_ne.
  Coercion ne2nf : vdash_ne >-> vdash_nf.

  Inductive vdash_con : con A -> con A -> Prop :=
  | vdash_empty : forall G, G |-- (@empty A)
  | vdash_ext : forall G D P, G |-- D -> G |-v P -> G |-- (D # P)

    where " G |-- D " := (vdash_con G D).

  Lemma vdash_var_t : forall G T, G |-v T -> G |- T.
  Proof.
    induction 1 ; constructor ; auto.
  Qed.

  Coercion vdash_var_t : vdash_var >-> vdash.

  Scheme ne_nf_ind := Induction for vdash_ne Sort Prop
  with nf_ne_ind := Induction for vdash_nf Sort Prop.

  Combined Scheme ne_nf_mutind from ne_nf_ind,nf_ne_ind.

  Scheme var_ne_nf_ind := Induction for vdash_var Sort Prop
  with ne_nf_var_ind := Induction for vdash_ne Sort Prop
  with nf_var_ne_ind := Induction for vdash_nf Sort Prop.

  Combined Scheme var_ne_nf_mutind from var_ne_nf_ind, ne_nf_var_ind, nf_var_ne_ind.

  Lemma vdash_ne_nf_t : (forall G T, G |-ne T -> G |- T) /\ (forall G T, G |-nf T -> G |- T).
  Proof.
    apply ne_nf_mutind ; intros ; try constructor ; auto.
    exact v.
    eapply app with P ; auto.
  Qed.

  Lemma vdash_ne_t : forall G T, G |-ne T -> G |- T. 
  Proof proj1 vdash_ne_nf_t.

  Lemma vdash_nf_t : forall G T, G |-nf T -> G |- T.  
  Proof proj2 vdash_ne_nf_t.

  Coercion vdash_ne_t : vdash_ne >-> vdash.
  Coercion vdash_nf_t : vdash_nf >-> vdash.

  Lemma weak_vdash_con : forall G D P, G |-- D -> G # P |-- D.
  Proof with auto.
    induction 1 ; simpl ; intros.

    constructor.

    constructor.
    assumption.
    constructor.
    assumption.
  Qed.

  Lemma id_vdash_con : forall G, G |-- G.
  Proof with auto.
    induction G ; simpl ; intros...

    constructor.
    constructor.
    apply weak_vdash_con.
    assumption.

    constructor.
  Qed.

  Lemma subst_vdash_con : forall D P, D |- P -> forall G, G |-- D -> G |- P.
  Proof with auto.
    induction 1 ; intros.

    inversion H ; subst.
    exact H4.

    apply IHvdash.
    inversion H0.
    assumption.

    apply abs.
    apply IHvdash.
    constructor.
    apply weak_vdash_con.
    assumption.
    constructor.

    apply app with P.
    apply IHvdash1...
    apply IHvdash2...
  Qed.

  Lemma subst_vdash_var_con : forall D P, D |-v P -> forall G, G |-- D -> G |-v P.
  Proof with auto.
    induction 1 ; intros.

    inversion H ; subst.
    exact H4.

    apply IHvdash_var.
    inversion H0.
    assumption.
  Qed.

  Lemma subst_vdash_ne_nf_con : (forall D P, D |-ne P -> forall G, G |-- D -> G |-ne P) /\
    (forall D P, D |-nf P -> forall G, G |-- D -> G |-nf P).
  Proof with auto.
    apply ne_nf_mutind ; intros.

    exact (subst_vdash_var_con v H).

    apply n_app with P ; auto.

    exact (H _ H0).

    apply n_abs.
    apply H.
    constructor.
    apply weak_vdash_con.
    assumption.
    constructor.
  Qed.

  Lemma subst_vdash_ne_con : forall D P, D |-ne P -> forall G, G |-- D -> G |-ne P.
  Proof proj1 (subst_vdash_ne_nf_con). 

  Lemma subst_vdash_nf_con : forall D P, D |-nf P -> forall G, G |-- D -> G |-nf P.
  Proof proj2 (subst_vdash_ne_nf_con). 

  Lemma vdash_con_trans : forall G D P, G |-- D -> D |-- P -> G |-- P.
  Proof with auto.
    induction 2.

    constructor.

    constructor.
    apply (IHvdash_con H).

    apply subst_vdash_var_con with G0...
  Qed.

  Lemma subst_vdash_at : forall G D, D |-- G -> forall a, G |- a -> D |- a.
  Proof.
    simpl ; intros.
    apply subst_vdash_con with G ; auto.
  Qed.

  Lemma subst_vdash_at_nf : forall G D, D |-- G -> forall a, G |-nf a -> D |-nf a.
  Proof.
    simpl ; intros.
    apply subst_vdash_nf_con with G ; auto.
  Qed.

  Definition U : kripke A :=
    @mkKripke A (con A) (vdash_con) (id_vdash_con) (vdash_con_trans) 
    (fun G a => G |- atom a) (fun G D fGD a => @subst_vdash_at _ _ fGD (atom a)).

  Definition Unf : kripke A :=
    @mkKripke A (con A) (vdash_con) (id_vdash_con) (vdash_con_trans) 
    (fun G a => G |-nf atom a) (fun G D fGD a => @subst_vdash_at_nf _ _ fGD (atom a)).

  Lemma qu : forall P, (forall G, force_prop U G P -> G |- P) /\
    (forall G, G |- P -> force_prop U G P).
  Proof.
    induction P.

    simpl.
    split ; intros ; trivial.

    simpl in *.
    split ; intros.

    constructor.
    destruct IHP2 as [H0 H1].
    apply H0.
    apply H.
    apply weak_vdash_con.
    apply id_vdash_con.

    destruct IHP1 as [H2 H3].
    apply H3.
    apply ax.

    destruct IHP1 as [H4 H5] ; destruct IHP2 as [H2 H3].
    apply H3.
    apply app with P1.
    apply subst_vdash_con with G.
    assumption.
    assumption.

    apply H4.
    assumption.
  Defined.

  Lemma ucon : forall G D, vdash_con G D -> force_con U G D.
  Proof.
    induction 1 ; intros.

    constructor.

    constructor.
    assumption.

    apply (proj2 (qu P)).
    exact H0.
  Qed.

  Lemma completeness : forall G P, (forall w, force_con U w G -> force_prop U w P) -> G |- P.
  Proof.
    intros.
    apply (proj1 (qu P)).
    apply H.
    apply ucon.
    apply id_vdash_con.
  Qed.

  Lemma qu_nf : forall P, (forall G, force_prop Unf G P -> G |-nf P) /\
    (forall G, G |-ne P -> force_prop Unf G P).
  Proof with auto.
    induction P.

    simpl.
    split ; intros ; trivial.

    exact H.

    simpl in *.
    destruct IHP1 as [H0 H1].
    destruct IHP2 as [H2 H3].
    
    split ; intros.

    apply n_abs.
    apply H2.
    apply H.
    apply weak_vdash_con.
    apply id_vdash_con.

    apply H1.
    constructor.
    constructor.

    apply H3.
    apply n_app with P1.
    apply subst_vdash_ne_con with G...

    apply H0.
    apply H5.
  Defined.

  Lemma ucon_nf : forall G D, vdash_con G D -> force_con Unf G D.
  Proof.
    induction 1 ; intros.

    constructor.

    constructor.
    assumption.

    apply (proj2 (qu_nf P)).
    exact H0.
  Qed.

  Lemma completeness_nf : forall G P, (forall w, force_con Unf w G -> force_prop Unf w P) -> G |-nf P.
  Proof.
    intros.
    apply (proj1 (qu_nf P)).
    apply H.
    apply ucon_nf.
    apply id_vdash_con.
  Qed.

  Lemma nf : forall G P, G |- P -> G |-nf P.
  Proof.
    intros.
    apply completeness_nf.
    intros.
    apply soundness with G.
    exact H.
    assumption.
  Qed.
End Completeness.

Notation " G |-- D " := (vdash_con G D) (at level 30).
Notation " G |-v t " := (vdash_var G t) (at level 30).
Notation " G |-ne t " := (vdash_ne G t) (at level 30).
Notation " G |-nf t " := (vdash_nf G t) (at level 30).

Section Peirce.
  Variable A : Set.
  Variables a b : A.
  Coercion atomic := @atom A.
  
  Definition peirce := ((a ==> b) ==> a) ==> a.
  
  Hypothesis diff_a_b : a <> b.

  Section Model.
    Definition worlds := bool.
    
    Definition le_worlds x y : Prop := 
      match x, y with
        | true, _ => True
        | _, false => True
        | _, _ => False
      end.

    Lemma le_id : forall x, le_worlds x x.
    Proof.
      induction x ; simpl ; auto.
    Qed.

    Lemma le_trans : forall x y z, le_worlds x y -> le_worlds y z -> le_worlds x z.
    Proof.
      induction x ; induction y ; induction z ; simpl ; auto.
    Qed.

    Inductive world_force : worlds -> A -> Prop :=
    | force_true : world_force true a.

    Lemma force_mon : forall w w', le_worlds w' w -> forall a, world_force w a -> world_force w' a.
    Proof.
      induction w ; induction w' ; simpl ; intros ; auto.
      inversion H.
      inversion H0.
    Qed.

    Definition model := mkKripke le_worlds le_id le_trans world_force force_mon.
  End Model.

  Lemma force_false : forall a, ~ world_force false a.
  Proof.
    intros a0 H ; inversion H.
  Qed.
  
  Notation " P ||- C " := (force_prop model P C) (at level 30).
  
  Ltac poses c := let H := fresh "H" in assert(H:=c).

  (** Proving the non-derivability of Peirce's law using the soundness of the kripke model. *)

  Lemma no_peirce : ~ (@empty A |- peirce).
  Proof with subst ; auto.
    red ; intros.
    assert (Hf:=soundness model H false I).

    assert (~ false ||- a ==> b).
    simpl ; red ; intros.
    pose (H0 true I force_true).
    inversion w.
    contradiction.
    assert (false ||- (a ==> b) ==> a).
    simpl ; intros.
    simpl in *.
    destruct w'.
    constructor.
    elim (H0 H2).

    assert (~ false ||- b).
    red ; intros.
    inversion H2.

    assert (~ false ||- peirce).
    unfold peirce.
    red ; intros.
    pose (H3 false I H1).
    simpl in f.
    inversion f.
    
    apply (H3 Hf).
  Qed.

  (** A shorter proof - we need not prove [~ false ||- b]. *)
  Lemma no_peirce' : ~ (@empty A |- peirce).
  Proof with subst ; auto.
    unfold peirce ; red ; intros.
    assert (Hf:=soundness model H false I).

    assert (~ false ||- a ==> b).
    simpl ; red ; intros.
    pose (H0 true I force_true).
    inversion w.
    contradiction.

    assert (false ||- (a ==> b) ==> a).
    simpl ; intros.
    simpl in *.
    destruct w'.
    constructor.
    elim (H0 H2).

    pose (Hf false I H1).
    simpl in f.
    inversion f.
  Qed.

  (** Same proof using the characterisation of derivable formulas as normal forms. *)
  
  Require Import Coq.Program.Program.
  Lemma no_empty_ne : forall P, ~ (@empty A |-ne P).
  Proof.
    intros.
    intro.
    dependent induction H.
    inversion H.

    apply IHvdash_ne ; auto.
  Qed.

  Lemma vdash_var_single : forall (P Q : prop A), @empty A # P |-v Q -> P = Q.
  Proof.
    intros.
    inversion H ; subst ; auto.
    inversion H3.
  Qed.

  Implicit Types c d : A.

  (** Actually, not needed ! *)
(*   Lemma ne_nf_exchange : (forall G t, G |-ne t -> forall G' c d, G = (G' # c) # d -> (G' # d) # c |-ne t) /\ *)
(*     (forall G t, G |-nf t -> forall G' c d, G = (G' # c) # d -> (G' # d) # c |-nf t). *)
(*   Proof. *)
(*     apply ne_nf_mutind ; simpl ; intros ; subst. *)
(*     constructor ; auto. *)
(*     inversion v ; subst. *)
(*     apply v_weak ; constructor. *)
(*     inversion H2 ; subst. *)
(*     constructor. *)
(*     do 2 apply v_weak ; assumption. *)

(*     apply n_app with P ; auto. *)

(*     apply ne2nf. *)
(*     apply H ; auto. *)
(*     apply n_abs ; auto. *)
(*     apply H. *)
  
  (* TODO: needs exchange lemma for n_abs *)
(*   Lemma ne_nf_weak : (forall G t, G |-ne t -> forall c, G # c |-ne t) /\ *)
(*     (forall G t, G |-nf t -> forall c, G # c |-nf t). *)
(*   Proof. *)
(*     apply ne_nf_mutind ; simpl ; intros ; subst. *)
(*     constructor ; auto. *)
(*     apply v_weak ; auto. *)
(*     apply n_app with P ; auto. *)

(*     apply ne2nf. *)
(*     apply H ; auto. *)
(*     apply n_abs ; auto. *)
(*   Admitted. *)

(*   Lemma ne_nf_impl : (forall G t, G |-ne t -> forall c d, t = c ==> d -> G # c |-ne d) /\ *)
(*     (forall G t, G |-nf t -> forall c d, t = c ==> d -> G # c |-nf d). *)
(*   Proof. *)
(*     apply ne_nf_mutind ; simpl ; intros ; subst. *)
    
(*     apply n_app with c. *)
(*     apply v2ne. *)
(*     apply v_weak ; auto. *)
(*     repeat constructor. *)
    
(*     (* Is there another way ? *) *)
(*     apply n_app with c ; auto. *)
(*     apply n_app with P ; auto. *)
(*     apply (proj1 ne_nf_weak) ; auto. *)
(*     apply (proj2 ne_nf_weak) ; auto. *)
(*     repeat constructor. *)

(*     pose (H c d (refl_equal (c ==> d))). *)
(*     constructor ; auto. *)

(*     inversion H0 ; subst. *)
(*     assumption. *)
(*   Qed. *)

  (** Needed to prove inversion lemmas on neutral and normal judgements. *)
  Fixpoint arity_ends (c : prop A) a : Prop :=
    match c with
      | atom x => a = x
      | p ==> q => arity_ends q a
    end.
  
  Fixpoint exists_impl G a {struct G} : Prop :=
    match G with
      | empty => False
      | G' # c => exists_impl G' a \/ arity_ends c a
    end.

  Lemma var_ne_nf_atom : 
    (forall G t, G |-v t -> forall a : A, arity_ends t a -> exists_impl G a) /\
    (forall G t, G |-ne t -> forall a : A, arity_ends t a -> exists_impl G a) /\
    (forall G t, G |-nf t -> forall a : A, arity_ends t a -> exists_impl G a \/ arity_ends t a).
  Proof.
    apply var_ne_nf_mutind ; simpl ; intros ; subst ; try discriminate.
    
    right ; simpl ; auto.
    
    left ; apply H ; auto.

    apply H ; auto.

    apply H ; auto.

    left ; apply H ; auto.

    right ; auto.
  Qed.

  Lemma ne_atom : forall G (a : A), G |-ne a -> exists_impl G a.
  Proof.
    intros.
    apply (proj1 (proj2 var_ne_nf_atom)) with a0 ; auto.
    simpl ; reflexivity.
  Qed.
  
  Lemma nf_atom : forall G (x : A), G |-nf x -> exists_impl G x.
  Proof.
    intros G x H.
    unfold atomic in * ; dependent induction H.
    apply ne_atom ; auto.
  Qed.

  Lemma ne_peirce: forall G R,
    G |-ne R -> forall a b, G = empty A # (atom a ==> atom b) ==> atom a -> R = (atom a ==> atom b) ==> atom a \/ R = atom a.
  Proof.
    induction 1 ; intros ; subst.
    inversion H ; subst.
    left ; auto.
    inversion H3.
    
    destruct (IHvdash_ne a0 b0) ; auto.
    inversion H1 ; subst.
    right ; auto.

    discriminate.
  Qed.
  
  Lemma no_peirce_nf : ~ (@empty A |-nf peirce).
  Proof with subst ; auto.
    unfold peirce ; intro.
    inversion H ; subst.
    eapply no_empty_ne ; apply H0.
    
    inversion H2...
    
    inversion H0...
    pose (vdash_var_single H1).
    discriminate.

    destruct (ne_peirce H1 (a:=a) (b:=b))...
    inversion H4 ; subst.
    inversion H3...
    destruct (ne_peirce H5 (a:=a) (b:=b)) ; subst ; auto ; try discriminate.
    pose (nf_atom H7).
    simpl in e.
    intuition.
    
    discriminate.
  Qed.    

End Peirce.

Require Coq.Program.Program.

Section Substitution.
  Variable A : Set.
  
  Reserved Notation " G ++ D " (at level 30).
  
  Fixpoint append (G D : con A) :=
    match D with
      | empty => G
      | D' # t => (G ++ D') # t
    end
    
    where "G ++ D" := (append G D).

  Program Fixpoint subst_rec (G D : con A) (P Q : prop A) (t : G # P ++ D |- Q) (u : G |- P) 
    {struct t} : G ++ D |- Q :=
    match t with
      | ax _ _ => match D with empty => u | D' # P => ax (G ++ D') P end
      | weak D' _ U t => match D with empty => t | D' # P => weak U (@subst_rec G D' _ _ t u) end
      | abs _ tau tau' t => abs (@subst_rec G (D # tau) _ _ t u)
      | app _ tau tau' f e => app (subst_rec _ f u) (subst_rec _ e u)
    end.

  Solve Obligations using program_simpl ; intros ; simpl in * ; inversion Heq_anonymous ; reflexivity.

(*   Print subst_rec. *)
  
  Definition subst G := @subst_rec G (empty A).

  Inductive red (G : con A) (P : prop A) : (G |- P) -> (G |- P) -> Prop :=
    red_beta : forall P' (t : G # P' |- P) (u : G |- P'), 
      red (app (abs t) u) (subst t u).

  Inductive redstar (G : con A) (P : prop A) : (G |- P) -> (G |- P) -> Prop :=
  | redstar_refl : forall t, redstar t t
  | redstar_trans : forall t u v, red t u -> redstar u v -> redstar t v.

End Substitution.