(* Lab on Propositional Logic in Coq *)
(* CS3234, Martin Henz and Aquinas Hobor *)

(* A little black magic to make sure that "*" is the product constructor on types
    instead of the multiplication operator on nat. *)
Open Local Scope type_scope.

(* Some useful tactics *)
Tactic Notation "spec" hyp(H) :=
  match type of H with ?a -> _ => 
    let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end.

Tactic Notation "spec" hyp(H) constr(a) :=
  (generalize (H a); clear H; intro H). 

Tactic Notation "spec" hyp(H) constr(a) constr(b) :=
  (generalize (H a b); clear H; intro H).

 Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) :=
  (generalize (H a b c); clear H; intro H).

Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) :=
  (generalize (H a b c d); clear H; intro H).

Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) :=
  (generalize (H a b c d e); clear H; intro H).

Ltac remembertac2 x a :=
  let x := fresh x in
  let H := fresh "Heq" x in
  (set (x:=a) in *; assert (H: a=x) by reflexivity; clearbody x).

Tactic Notation "cases" constr(a) :=
  let x := fresh in (remembertac2 x a; destruct x).

Require ClassicalFacts.  (* no axioms in this line *)
Require Export Coq.Logic.ClassicalChoice. 
     (* Axioms dependent_unique_choice, relational_choice *)

Axiom dep_extensionality:
 forall (A: Type) (B: A -> Type) (f g : forall x: A, B x),  (forall x, f x = g x) -> f = g.
Implicit Arguments dep_extensionality.

Axiom prop_ext: ClassicalFacts.prop_extensionality.
Implicit Arguments prop_ext.

Inductive Num : Type :=
  | Zero : Num
  | Succ : Num -> Num.

Definition Atom : Type := Num.

Definition p_0 : Atom := Zero.
Definition p_1 : Atom := Succ Zero.
Definition p_2 : Atom := Succ (Succ Zero).

Record Bool : Type :=
  | T : Bool
  | F : Bool.

Definition Valuation : Type := Atom -> Bool.

Definition exampleValuation : Valuation :=
  fun a : Atom => match a with
    | Zero                     => T   (* p_0       *)
    | Succ Zero                => F   (* p_1       *)
    | Succ (Succ Zero)         => T   (* p_2       *)
    | _                        => F   (* all other *)
  end.

Inductive PropFormula : Type :=
  | propTop : PropFormula
  | propBot : PropFormula
  | propAtom : Atom -> PropFormula
  | propNeg : PropFormula -> PropFormula
  | propConj : PropFormula -> PropFormula -> PropFormula
  | propDisj : PropFormula -> PropFormula -> PropFormula
  | propImpl : PropFormula -> PropFormula -> PropFormula.

Definition exampleFormula : PropFormula :=
  propDisj (propNeg (propAtom p_2)) 
                 (propImpl (propConj (propAtom p_1) propTop)
                                   propBot).

Fixpoint eval (f : PropFormula) (v : Valuation) : Bool :=
  match f with
  | propTop =>
    T
  | propBot =>
    F
  | propAtom a => 
    v(a)
  | propNeg f1 =>
    match (eval f1 v) with
      | F => T
      | T => F
      end
  | propConj f1 f2 =>
    match (eval f1 v, eval f2 v) with
     | (F, F) => F
     | (F, T) => F
     | (T, F) => F
     | (T, T) => T
    end
  | propDisj f1 f2 =>
    match (eval f1 v, eval f2 v) with
     | (F, F) => F
     | (F, T) => T
     | (T, F) => T
     | (T, T) => T
    end
  | propImpl f1 f2 =>
    match (eval f1 v, eval f2 v) with
     | (F, F) => T
     | (F, T) => T
     | (T, F) => F
     | (T, T) => T
    end
  end.

Goal (eval exampleFormula exampleValuation) = T.
  reflexivity.
Qed.

Module Type PROP_PROOF_RULES.

Section RULES.
Variable v : Valuation.
  
  Definition holds (f : PropFormula) : Prop :=
    eval f v = T.

  Axiom Top_I :
    holds propTop.

  Axiom Conj_I : forall f1 f2,
    holds f1 ->
    holds f2 ->
    holds (propConj f1 f2).

  Axiom Conj_E1 : forall f1 f2,
    holds (propConj f1 f2) ->
    holds f1.

  Axiom Conj_E2 : forall f1 f2,
    holds (propConj f1 f2) ->
    holds f2.

  Axiom NegNeg_E : forall f,
    holds (propNeg (propNeg f)) ->
    holds f.

  Axiom Impl_I : forall f1 f2,
    (holds f1 -> holds f2) ->
    holds (propImpl f1 f2).

  Axiom Impl_E : forall f1 f2,
    holds (propImpl f1 f2) ->
    holds f1 ->
    holds f2.

  Axiom Disj_I1 : forall f1 f2,
    holds f1 ->
    holds (propDisj f1 f2).

  Axiom Disj_I2 : forall f1 f2,
    holds f2 ->
    holds (propDisj f1 f2).

  Axiom Disj_E : forall f1 f2 f3,
    holds (propDisj f1 f2) ->
    (holds f1 -> holds f3) ->
    (holds f2 -> holds f3) ->
    holds f3.

  Axiom Bot_E : forall f,
    holds propBot -> 
    holds f.

  Axiom Neg_E : forall f,
    holds f ->
    holds (propNeg f) -> 
    holds propBot.

  Axiom Neg_I : forall f,
    (holds f -> holds propBot) ->
    holds (propNeg f).

End RULES.
End PROP_PROOF_RULES.









(* Lab, Part 1 *)

(* Above we gave a set of definitions and axioms that defined natural 
   deduction in the context of propositional logic.  In analogy to, say,
   Java, we have given an *interface* to propositional logic---the Coq
   keyword to declare an interface is "Module Type".
   
   You might wonder: in Java after defining an Interface, we often next
   define an Object that implements that Interface.  Does Coq have the
   same idea?
   
   The answer is yes.  It is possible to provide an *implementation*
   of a Module Type -- such an implementation is indicated with
   the keyword "Module", as follows: *)

Module Proving_ProofRules : PROP_PROOF_RULES.

(* We are now defining a Module, Proving_ProofRules, that must
    match the interface PROP_PROOF_RULES.  The first few lines
    are just copies from the interface: *)

Section RULES.
Variable v : Valuation.
  
  Definition holds (f : PropFormula) : Prop :=
    eval f v = T.

(* But now the real work begins.  Everywhere that we wrote "Axiom"
    in the PROP_PROOF_RULES interface, we must now write "Lemma"
    and provide a proof.  Suppose we do not, and instead try to finish
    the Module Proving_ProofRules, as follows: (uncomment this next 
    line, including both the End RULES and the End Proving_ProofRules,
    try it out, then recomment both Ends and continue) *)

(* End RULES. End Proving_ProofRules. *)

(* You should get some kind of weird error message, that includes the
    line: 
         The field Top_I is missing in Top.Proving_ProofRules.
    In other words, the axiom "Top_I" is promised by the interface
    PROP_PROOF_RULES, but is missing from the implementation of
    Proving_ProofRules.  We can't close the module yet. *)

(* So we might as well start with Top_I.  We declare a lemma with the
    exact same name and form as in the interface: *)
  Lemma Top_I :
    holds propTop.
(* And now we must provide the proof.  Notice some of the tactics used
    since you will have to do this for some of the other axioms. *)
  Proof.
    unfold holds.
    simpl.
    reflexivity.
  Qed.
  
(* Ok, that wasn't too bad, but maybe we should do a few more to 
    let you see what they are like.  *)

  Lemma Conj_I : forall f1 f2,
    holds f1 ->
    holds f2 ->
    holds (propConj f1 f2).
  Proof.
    intros.
    unfold holds.
    simpl.
    unfold holds in H.
    rewrite H.
    unfold holds in H0.
    rewrite H0.
    reflexivity.
  Qed.

  Lemma Conj_E1 : forall f1 f2,
    holds (propConj f1 f2) ->
    holds f1.
  Proof.
    intros.
    red in H. red.
    (* Here we will try a new tactic, called "cases" *)
    cases (eval f1 v).
    (* Notice that we now have two goals.  We are in the first goal, where
        eval f1 v = T; the second goal will come later, when eval f1 v = F.
        Also notice that we have a new hypothesis, "HeqH0", that says that
        "eval f1 v = T".  There are other ways to do cases, including tactics
        like "destruct".  Experiment if you like, but "cases" should be a little
        bit less error-prone than some of the others. *)
    reflexivity.  (* Of course, in the first case, things are easy! *)
    (* Now we are in the second case, and the goal is impossible!  We
        better hope we can find a contradiction in the premises. *)
    simpl in H.
    rewrite HeqH0 in H.
    (* This is looking a little promising -- either way "eval f2 v" goes,
        we should have "F = T" as a premise. *)
    cases (eval f2 v). (* Again generates 2 cases *)
    (* Now we have two choices.  One choice is that we can just say, *)
    assumption.
    (* The other choice is that we can tell Coq that there is a contradiction
        in the premises.  There are a lot of tactics for this that differ in
        certain ways.  The easiest way to do this here is the "discriminate"
        tactic, which looks for equalities in the hypothesis thare are impossible
        and if it finds any, solves the goal. *)
    discriminate.
  Qed.
  
  (* Ok, now your turn for the next one; it is similar to the previous: *)
  Lemma Conj_E2 : forall f1 f2,
    holds (propConj f1 f2) ->
    holds f2.
  Proof.
    admit.
  Qed.
  
  (* Why don't you try this one, too! *)
  Lemma NegNeg_E : forall f,
    holds (propNeg (propNeg f)) ->
    holds f.
  Proof.
    admit.
  Qed.
  
  (* This next one is a little different, since it has an implication "in 
      the middle." *)
  Lemma Impl_I : forall f1 f2,
    (holds f1 -> holds f2) ->
    holds (propImpl f1 f2).
  Proof.
    intros.
    red.
    simpl.
    cases (eval f1 v).
    unfold holds in H.
    (* Notice how we use the "spec" tactic to do MP in our hypothesis. *)
    spec H HeqH0.
    rewrite H.
    reflexivity.
    cases (eval f2 v); trivial.
  Qed.
  
  (* Why don't you give this one a try: *)
  Lemma Impl_E : forall f1 f2,
    holds (propImpl f1 f2) ->
    holds f1 ->
    holds f2.
  Proof.
    admit.
  Qed.

  (* Being the nice guy that I am, I'll do this next one for you... *)
  Lemma Disj_I1 : forall f1 f2,
    holds f1 ->
    holds (propDisj f1 f2).
  Proof.
    intros.
    red. simpl.
    red in H.
    rewrite H.
    cases (eval f2 v); trivial.
  Qed.
  
  (* This one is very similar, you do it: *)
  Lemma Disj_I2 : forall f1 f2,
    holds f2 ->
    holds (propDisj f1 f2).
  Proof.
    admit.
  Qed.
  
  (* This one is harder, but you can do it! *)
  Lemma Disj_E : forall f1 f2 f3,
    holds (propDisj f1 f2) ->
    (holds f1 -> holds f3) ->
    (holds f2 -> holds f3) ->
    holds f3.
  Proof.
    admit.
  Qed.
  
  (* The "discriminate" tactic is vital here. *)
  Lemma Bot_E : forall f,
    holds propBot -> 
    holds f.
  Proof.
    admit.
  Qed.
  
  (* I will do the next one... *)
  Lemma Neg_E : forall f,
    holds f ->
    holds (propNeg f) -> 
    holds propBot.
  Proof.
    intros.
    red in H, H0. simpl in H0.
    rewrite H in H0.
    discriminate.
  Qed.
  
  (* ... as long as you do the last one. *)
  Lemma Neg_I : forall f,
    (holds f -> holds propBot) ->
    holds (propNeg f).
  Proof.
    admit.
  Qed.

(* We've now proved all the rules -- in other words, we have provided
    an implementation to the PROP_PROOF_RULES interface.  Thus,
    we can close the Module Proving_ProofRules without trouble: *)

End RULES.

End Proving_ProofRules.

(* Actually, this is a very important mathematical fact -- that we were
    able to provide an implementation (in mathematics, this is called a
    "model") for our axioms.  Once we know a model (implementation)
    for a set of axioms exists, then we call the axioms "sound".  So,
    we have just proved the soundness of propositional logic, which is
    pretty good of us.  We will discuss soundness a bit more in class
    and also a related property called "completeness". *)

(* Lab, part 2 *)

(* For the remainder of the lab (and at home if you like), we will just do
    some extra problems using our now-proved-sound axioms.  This is
    just for extra practice. *)

(* To use our model, we want to "Import" it: *)
Import Proving_ProofRules.

(* To avoid cheating, we use this to make sure we can't unfold holds
    any more... *)
Opaque holds.

(* Now we can use the rules very easily.  For example, here is a proof
    of P /\ Q -> Q /\ P *)
Lemma ConjComm: forall v P Q,
  holds v (propImpl (propConj P Q) (propConj Q P)).
Proof.
  intros.
  apply Impl_I. (* We use our lemma defined above! *)
  intro.
  apply Conj_I. (* We use our lemma defined above! *)
  apply Conj_E2 with P. (* We use our lemma defined above! Note we
                                             must provide "P" since Coq can't guess it. *)
  trivial.
  apply Conj_E1 with Q. (* etc. *)
  trivial.
Qed.

(* This was done in the notes already, just here for your reference *)
Lemma NegNeg_I : forall v P,
  holds v P ->
  holds v (propNeg (propNeg P)).
Proof.
  intros.
  apply Neg_I. (* Our lemma defined above *)
  intro.
  apply Neg_E with P. (* etc. *)
  trivial.
  trivial.
Qed.

Lemma DisjComm: forall v P Q,
  holds v (propImpl (propDisj P Q) (propDisj Q P)).
Proof.
  admit.
Qed.

Lemma DisjAssoc: forall v P Q R,
  holds v (propImpl (propDisj P (propDisj Q R)) (propDisj (propDisj P Q) R)).
Proof.
  admit.
Qed.

(* This one is harder and worth doing for practice in the lab or at home. *)
Lemma deMorgan1 : forall v P Q,
  holds v (propImpl (propDisj (propNeg P) (propNeg Q)) (propNeg (propConj P Q))).
Proof.
  admit.
Qed.

(* We won't prove this one now, let's just be able to use it if we want to... *)
Axiom LEM : forall v P,
  holds v (propDisj P (propNeg P)).

(* This one is a little tricky.  You will need LEM or NegNeg_E. *)
Lemma deMorgan2 : forall v P Q,
  holds v (propImpl (propNeg (propConj P Q)) (propDisj (propNeg P) (propNeg Q))).
Proof.
  admit.
Qed.

(* End of Lab Material *)