(*---- In this class session we did a variety of logic predicate calculus proofs -----*) 
(*----   to show the details of pattern matching and proof terms                 -----*) 

(*-- A reminder: Haskell and Rocq have rich syntactic notations, types, and
         constructors. Notations are typically infix syntax for parametrized types, e.g.,
	 A/\B for (and A B). Constructors are /the only way/ that values of these types
	 can come into being, e.g., (conj a b) where a is of type A and b is of type B,
	 a : A, b : B is the only way to make an (and A B), a.k.a. A/\B.
     Because of these definitions, any value of type A/\B will need to be pattern-matched
         on (conj a b) to get any work done on it (unless you just want to pass it along
	 or use it as a whole, e.g., in an identity function such as (fun x => x) or
	 have a function that applies to it exactly, e.g, ~(A/\B) to obtain False --*)
       
Locate "/\".  (* Where's the syntax defined and what it translates to. We find "and" *)

Locate and.   (* How is the type constructed. We find "conj" the constructor *)
Print and.

Locate Library Corelib.Init.Logic.  (* This is the original library file *)

Print conj.   (* Doesn't give us anything new over the definition of "and" *)

(* Multiple variants of the same simple pattern match and construct *)

Theorem eConjL : forall A B : Prop , A/\B -> A.
Proof (fun A B ab => match ab with conj a _ => a end).

Check eConjL.

Theorem eConjR : forall A B : Prop , A/\B -> B.
Proof (fun A B ab => match ab with conj _ b  => b end).

Check eConjR.

Theorem and_swap'' : forall A B : Prop, A /\ B -> B /\ A.
Proof (fun A B ab => match ab with conj a b => conj b a end).

(* Here is a different way to construct proof objects. This way is
     gradual, with each tactic hopefully bringing you closer to
     constructing a full proof term. You can see the current state
     of the proof term being constructed with Show Proof. You will see
     lots of examples of these proofs in the library files such as Logic.v *)

(* Step through this proof: *) 

Theorem elimConjL : forall A B : Prop, A /\ B -> A .
Proof. 
  intros.            (* introduces the lambda function that will be the proof term *)
  Show Proof.
  Show Match and.    (* shows the match pattern for the type 'and'. *) 
  destruct H.        (* inserts the same pattern as above into the proof term body *)
  Show Proof.
  exact H.           (* selects "a" to fulfill the goal of producing an A *)
  Show Proof.
Qed.

(**    The generated proof term is a bit more complex than our previously hand-written one,
         but it does the same thing:
(fun (A B : Prop) (H : A /\ B) =>
 match H with
 | conj x x0 => (fun (H0 : A) (_ : B) => H0) x x0
 end)
**)

(* Let's try another very similar example. Note that A/\B/\C is A/\(B/\C) due to how
    /\ is defined to the parser, right-associative. Rocq's "Set Printing Parentheses." mode
    and RocqIDE's View mode make that explicit. *)
    
Theorem elim3 : forall A B C : Prop , A /\ B /\ C -> C.
Proof (fun A B C abc => match abc with 
    conj _ z => match z with conj _ c => c end
  end).
  
Check elim3.      

(* Another one. The shortest proof term: *)

Theorem elim3a : forall A : Prop, A /\ A /\ A -> A .
Proof (fun A aaa => elim3 A A A aaa).

(* An even simpler match: *)

Theorem elim3a' : forall A : Prop, A /\ A /\ A -> A .
Proof (fun A aaa => match aaa with conj a _ => a end).

(* Try: *)
(* Set Printing Parentheses. *)
(* Set Printing Implicit. *)
(* Set Printing All. *)

(* Unset with: *)
(* Unset Printing Parentheses *)

(* Now for the logical Disjunction *)

Locate "\/".

Print or.

(**
Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B.

Arguments or (A B)%type_scope
Arguments or_introl [A B]%type_scope _, [_] _ _
Arguments or_intror [A B]%type_scope _, _ [_] _
**)


(** In an important distinction: A/\B had only one constructor, A\/B has two.
     So (almost) any proof involving A\/B must consider two alternatives
     of how a value of type (or A B) aka A\/B might've been constructed, and
     likely have two different proofs based on it: *) 
    
Theorem disj_swap : forall A B : Prop, A \/ B -> B \/ A.
Proof (fun A B a_b => match a_b with
             or_introl a => or_intror a     (* an A\/B came from an A. Then make B\/A with that a *)
          |  or_intror b => or_introl b     (* that A\/B came from B. Make B\/A with that b *)
        end).

(* The same with the tactics. *)

Theorem disj_swap' : forall A B : Prop, A \/ B -> B \/ A.
Proof.
   intros.
   destruct H.
   Show Proof.
   right.        (* commit to making the goal B\/A with the right part of it *)
   exact H.         (* ... and make it with H : A , a value of type A *)
   left.         (* commit to making the goal B\/A with the right part of it *)
   Show Proof.      (* symmetrically for H : B *)
   exact H.
Qed.   

(* Composition *)

(* Note: the final A->C does not need ()s . So we are really looking at
        (B->C)->(A->B)->A->C.
  
   This is hugely helpful for the proofs, because our parameters/premises can
     be interpreted as having A and A->B and B->C to make a C from. This treatment
     of A as an available parameter shows in both the hand-written proof term and
     Rocq's tactic helpers. Yet this is nothing other that currying. 
*)

Theorem comp : forall A B C : Prop, (B->C)->(A->B)->(A->C).
Proof (fun A B C b2c a2b a => b2c (a2b a)).

(* We could also write this, with an explicit lambda/fun made for  (A->C): *)

Theorem comp'' : forall A B C : Prop, (B->C)->(A->B)->(A->C).
Proof (fun A B C b2c a2b => (fun a => b2c (a2b a))).

(* The same with tactics: *)

Theorem comp' : forall A B C : Prop, (B->C)->(A->B)->(A->C).
Proof.
   intros.       (* Note that A gets picked up by intros *)
   Show Proof.
   apply H.      (* Apply is modus ponens. It matches the goal, and makes the premise the goal instead.  *)
                 (*  E.g.: if the goal is C and H is B->C then 'apply H' matches C and makes B the goal. *) 
   apply H0.
   exact H1.
   Show Proof.
Qed.
   
(* This is the S-combinator from lambda calculus *)

Theorem s_comb: forall P A B : Prop, (P->A->B) -> (P->A) -> P -> B . 
Proof (fun P A B p2a2b p2a p => (p2a2b p) (p2a p)).  

(* In lambda calculus notation, you'll remember it as
       \x \y \z . (x z)(y z)
   
    This combinator, together with the K combinator, is enough to build up all of lambda calculus.
     For example, S K K is I :

     (\xyz .(x z)(y z) (\x'y'.x')) (\x''y''.x'') -> (\yz . (\y'.z) (y z))(\x''y''.x'') ->
         \z (\y'.z) (\y''.z) -> \z . z
*)       

(* The definitions for \/ and -> allow us to derive the elimination rule for \/ *)

Theorem elimDisj: forall A B C : Prop , A\/B -> (A->C) -> (B->C) -> C.
Proof (fun A B C a_b a2c b2c => match a_b with
      | or_introl a => a2c a
      | or_intror b => b2c b 
      end).
      
Check elimDisj.

Show Match or.

(* Do this: *)

Theorem pqr: forall P Q R : Prop, (P -> (Q->R)) -> P/\Q -> R.
Proof. Admitted.  (* This is cheating. Replace Admitted with a real proof. *)

(* Note parens around P->(Q->R) . Without them it's a different proposition!
   On the other hand, P->Q->R is the same as P->(Q->R). Confirm it by hidings and
   displaying parentheses. 
 *)   


(* Distributivity. \/ is like addition , /\ is like multiplication  *)

Print right.

(* Do this too:

Theorem and_or_distr : forall A B C : Prop, A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
  
*)

(* ---- NOT and intros ----- *)

Locate "~".
Locate not.
About not.
Search not.

Print not. (* not = fun A : Prop => A -> False : Prop -> Prop *)

(* This may seem complicated, but in fact it's stunningly simple:
     we have A and (A->False) aka ~A . We need False. So we make it out of A and ~A,
     considering that ~A is exactly what makes a False from A: *)

Theorem notnot: forall A : Prop, A -> ~ ~ A.  (* A -> (A -> False) -> False *)
Proof (fun A a a2f => a2f a).

Check notnot.

(* It gets better: once we have constructed False, we can construct anything.
    This is how it happens technically in Rocq: since False has no constructors
    and no parameters, a match of False always succeeds---and unifies with any type.
    So this is the proof: *)

Theorem abs : forall A C:Prop, A -> ~ A -> C.
Proof (fun A C a a2f => match (a2f a) with end).

(* One key difference between the constructive/intuitionist and classical logic
    is that ~~P -> P does _not_ hold in constructive logic. Indeed,
    from (P->False)->False  nothing can be obtained, because one would need P
    or ~P to fire these implications. Neither can be assumed.

    By contrast, classical logic postulates  P\/~P. With this as an axiom,
    ~~P->P trivially follows. *)

(* Constructive logic does allow us to prove ~(A/\~A) -- "A and ~A cannot be true together"
     and also ~~(P\/~P)  as a consequence . Try this! *) 

(* ------- We stopped here --------- *)