Section Formulas.

  Variable Vars : Set.

  Inductive Formula : Set := 
  | Var : Vars -> Formula
  | Fal : Formula
  | Not : Formula -> Formula
  | And : Formula -> Formula -> Formula
  | Or : Formula -> Formula -> Formula
  | Imp : Formula -> Formula -> Formula.

  Infix "-->" := Imp (at level 50).
  Infix "\\//" := Or (at level 50).
  Infix "//\\" := And (at level 50).
  Notation "-, F" := (Not F) (at level 50). 

  Coercion Var : Vars >-> Formula.
  Variable p q:Vars.
  Definition pierce := ((p --> q) --> p) --> p.

  Require Import Bool.

  Section Semantics.

    Variable val : Vars -> bool.

    Fixpoint sem (f: Formula) {struct f} : bool :=
    match f with
    | Var x => val x
    | Fal => false
    | -, f => negb (sem f) 
    | f //\\ f' => sem f && sem f'
    | f \\// f' => sem f || sem f'
    | f --> f' => negb (sem f) || sem f'
    end.

  End Semantics.

  Notation "[[ f ] v ]" := (sem v f).

  Require Import List.

  Definition Formulas := list Formula.

  Section Gentzen.

    Reserved Notation "G ||- D" (at level 90).

    Inductive Gentzen : Formulas -> Formulas -> Prop :=

    | AKS : forall f,         f::nil ||- f ::nil

    | FAL :                     Fal::nil ||- nil

    | LO : forall G S f,         G ||- S                   
                                   (*--------*) ->
                                      f::G ||- S

    | PO : forall G S f,         G ||- S                   
                                   (*--------*) ->
                                      G ||- f::S

    | LW : forall G f1 f2 D S,   G++f1::f2::D ||- S
                                       (*----------------*) ->
                                         G++f2::f1::D ||- S

    | PW : forall G f1 f2 D S,   G ||- D++f1::f2::S
                                       (*----------------*) ->
                                         G ||- D++f2::f1::S

    | LS : forall G f1 f2 D S,   G++f1::f2::D ||- S
                                       (*----------------*) -> f1=f2 ->
                                           G++f2::D ||- S

    | PS : forall G f1 f2 D S,   G ||- D++f1::f2::S
                                       (*----------------*) -> f1=f2 ->
                                           G ||- D++f2::S

    | LN : forall G f S,              G ||- f::S 
                                      (*------------*) ->
                                          -,f::G ||- S

    | PN : forall G f S,               f::G ||- S 
                                      (*------------*) ->
                                        G ||-  -,f::S

    | LK : forall G f1 f2 S,       f1::f2::G ||- S
                                     (*---------------*) ->
                                         f1//\\f2 :: G ||- S

    | PK : forall G f1 f2 S,    G ||- f1::S      ->     G ||- f2::S
                                     (*--------------------------*) ->
                                              G ||- f1//\\f2 :: S

    | LA : forall G f1 f2 S,    f1::G ||- S      ->     f2::G ||- S
                                     (*--------------------------*) ->
                                              f1\\//f2 :: G ||- S

    | PA : forall G f1 f2 S,     G ||- f1::f2::S
                                     (*---------------*) ->
                                       G ||- f1\\//f2 :: S

    | LI : forall G f1 f2 S,    G ||- f1::S      ->     f2::G ||- S
                                     (*--------------------------*) ->
                                              f1-->f2 :: G ||- S

    | PI : forall G f1 f2 S,      f1::G ||- f2::S
                                     (*--------------*) ->
                                       G ||- f1-->f2::S

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



    Fixpoint OR (v:Vars -> bool) (G:Formulas) {struct G} : bool :=
    match G with
    | nil => false
    | f::G' => orb [[ f ]v] (OR v G')
    end.

    Lemma OR_W : forall v G D, 
      OR v (G++D) = OR v G || OR v D.
    induction G.
    simpl.
    auto.
    simpl.
    intros.
    rewrite IHG.
    auto with bool.
    Qed.

    Fixpoint AND (v:Vars -> bool) (G:Formulas) {struct G} : bool :=
    match G with
    | nil => true
    | f::G' => andb [[ f ]v] (AND v G')
    end.

    Lemma AND_W : forall v G D, 
      AND v (G++D) = AND v G && AND v D.
    induction G.
    simpl.
    auto.
    simpl.
    intros.
    rewrite IHG.
    auto with bool.
    Qed.


   Lemma bool_7 : forall b:bool, negb b=true -> b=false.
   Proof.
     destruct b; auto.
   Qed.
   
   Lemma bool_8 : forall b:bool, b=true -> b=false -> False.
   Proof.
     intro.
     intro.
     rewrite H.
     auto with bool.
   Qed.
   Hint Resolve bool_7 bool_8 : bool. 


   Ltac decomp := match goal with
   | |- _ && _ = true => apply andb_true_intro; split
   | H : _ && _ = true |- _ => destruct (andb_prop _ _ H); clear H
   | H : _ || _ = true |- _ => destruct (orb_prop _ _ H); clear H
   | |- _ || _ = true => apply orb_true_intro
   | H : negb ?f = true |- _ => assert (f=false); [auto with bool | clear H]
   | _ : ?b=true, _ : ?b=false |- _ => elim (bool_8 b); trivial   
   end.

   Ltac decont := match goal with 
   | |- context F [?f1 || ?f2 = true] => 
           let w:=context F [f1=true \/ f2=true] in
           assert w
   end.

   Ltac bum := repeat (repeat decomp; intuition).


    Lemma Gentzen_correct : forall v:Vars->bool, forall G D,
       G ||- D   ->   AND v G=true -> OR v D=true.
    Proof.
      simple induction 1; auto;
        intros until 1;
        repeat rewrite AND_W; repeat rewrite OR_W;
        simpl;
        intuition. 

        decomp.
        auto.
        
        apply H1.
        repeat decomp; assumption.
        
        info repeat decomp; intuition.

        apply H1; repeat decomp; intuition.
        rewrite H2; trivial.

        rewrite H2 in H4; repeat decomp; intuition.
        
        lapply H1.
        info decont.  (* tu match with context! *)
        info repeat decomp.
        intuition.
        info decomp.
        info decomp.
        intuition.
        intuition.
        info repeat decomp; assumption.

        bum.

        destruct [[f]v]; bum.

        apply H1; bum.

        bum.
        
        bum.

        bum.

        bum.

        destruct [[f1]v]; simpl; bum.
    Qed.

   End Gentzen.
End Formulas.