(**
    These examples illustrate Curry-Howard correspondence between types,
     proofs, and lambda terms, using simple Boolean logic proofs.

    You can follow online https://x80.org/jscoq2/examples/scratchpad.html  without installing Rocq.
     JsCoq's manual explains the keys: https://coq.vercel.app/ (start with Alt + ArrowDown to execute) 

    I do recommend you get your local copy of RocqIDE, though, because it's very nice.
 **)

(**
    Rocq implements Boolean logic entirely within its type system.
    Conjunction /\ , disjunction \/, and negation ~ are defined as the
      core library (the file Logic.v, we'll see it later).
    Implication -> is also modeled via the type system, but in
      a slightly more complicated manner.

    Amazingly (and due to the Curry-Howard correspondence) the result
     turns out to obey all rules of Predicate Logic Calculus.
    See https://cosc59.gitlab.io/rocq/Curry-Howard-Tutorial-ATCHC.pdf
     and https://groups.seas.harvard.edu/courses/cs152/2024sp/lectures/lec15-curryhoward.pdf for more examples and explanations.

    You could also look at
      https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html
     which explains the correspondence in terms of natural numbers constructed
     inductively from O with a successor constructor S (and that it all
     that definition allows, making it an inductive type. 
     
    Longer tutorials for a much deeper study:    
     https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/23-curryhoward.pdf
     https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/curry-howard.pdf 
**)

(* Finding definitions of things in Rocq is needed for survival. So
      Locate, Print, Locate Library, Print Notation, etc. are your best friends  *) 

Locate "/\".    (* Finding out what /\ means and where it is defined *)

(*> Notation "A /\ B" := (and A B) : type_scope *)

(* A /\ B is an infix form for the (and A B) , "and" is the type name*) 

Locate and.     

(* Inductive Corelib.Init.Logic.and *)

Locate Library Corelib.Init.Logic.

(* Corelib.Init.Logic has been loaded from file
/Applications/Rocq-Platform~9.0~2025.08.app/Contents/Resources/lib/coq/theories/Init/Logic.vo *)

(* The file on my computer is /Applications/Rocq-Platform~9.0~2025.08.app/Contents/Resources/lib/coq/theories/Init/Logic.v -- .vo is compiled object , .v is source. Totally look at it. *)

Print and.
(* Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B.

Arguments and (A B)%type_scope
Arguments conj [A B]%type_scope _ _ *)

(* So conj is the one and only constructor through which an /\ a.k.a. "and" is created.
   Any proof or any function involving "and" must pattern-match on conj *) 


Theorem and_swap : forall A B : Prop, A /\ B -> B /\ A.
Proof (fun A B '(conj a b) => conj b a ).  (* this form of pattern matching works iff there is only one constructor, no alternatives. It feels like cheating :) *)
(* and_swap is defined *)

Check and_swap. 
(* and_swap
     : forall A B : Prop, A /\ B -> B /\ A *)

(* It worked, we have a type! *)

(* Let's prove elimination rules for /\. Since these proofs are really just
   lambda functions, we can use them in other proofs too, like and_swap' *) 

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

Check eConjL.  
(* eConjL
     : forall A B : Prop, A /\ B -> A *)

(* it worked! *)

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

Check eConjR.
(* eConjR
     : forall A B : Prop, A /\ B -> B *)

(* This is where I made a mistake. I tried to use (eConjL ab) and (eConjR ab) and got a type mismatch.
   In retrospect, it's obvious: these lambda functions take 3 arguments, not 1! The type parameters A B
   must be given explicitly. These parameters have type Prop, and I was handing it ab of type A/\B instead.
   That explains the type mismatch. I discovered it right after the class. 

  BTW, I'm sure if I had pasted the function into Claude it'd have explained it as well. I am sure people 
   made this mistake before and wrote about it somewhere on the Internet :) *)      

Theorem and_swap' : forall A B : Prop, A /\ B -> B /\ A.
(*  *)
Proof (fun A B ab => conj (eConjR A B ab) (eConjL A B ab)).
(* and_swap' is defined *)

Check and_swap'.
(* and_swap'
     : forall A B : Prop, A /\ B -> B /\ A *)


(* It worked now, we have a type! *)

(* Another form could simply use match:  *)

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).

(* To be continued. Below are a few more examples of working with \/ , which has
    two constructors and hence a slightly more complex matching to do in proof terms. *) 

Locate "\/".
(* Notation "A \/ B" := (or A B) : type_scope (default interpretation) *)

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 _, _ [_] _ *)

Theorem disj_swap : forall A B : Prop, A \/ B -> B \/ A.
Proof (fun A B ab => match ab with 
                     | or_introl a => or_intror a 
                     | or_intror b => or_introl b 
                     end).

(* disj_swap is defined *)
  
Check disj_swap.
(* disj_swap
     : forall A B : Prop, A \/ B -> B \/ A *)

(* Composition *)

(* Note: the final A->C does not need ()s. So it's really (B->C)->(A->B)->A->C --and it helps hugely! *)
(*   Toggling Show Parentheses in RocqIDE helps to see this *)

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

Check comp.
(* comp
     : forall A B C : Prop, (B -> C) -> (A -> B) -> A -> C *)

(* This is the S-combinator from the tutorial: *)

Theorem s_comb: forall P A B : Prop, (P->A->B) -> (P->A) -> P -> B . 
(*  *)
Proof (fun P A B pab pa p => pab p (pa p)).
(* s_comb is defined *)

Check s_comb.
(* s_comb
     : forall P A B : Prop, (P -> A -> B) -> (P -> A) -> P -> B *)

(* Let's prove the disjunction elimination rule from the tutorial *)

Show Match or.  (* Reminding myself about the names of constructors for "or" *)
(* match # with
 | or_introl x =>
 | or_intror x =>
 end *)

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

Check elimDisj.
(* elimDisj
     : forall A B C : Prop, A \/ B -> (A -> C) -> (B -> C) -> C *)

(* NOT and intros. NOT is a little tricky, but proof terms make it simple. *)

Locate "~".
(* Notation "~ x" := (not x) : type_scope (default interpretation) *)

Locate not.
(* Constant Coq.Init.Logic.not *)

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

Arguments not A%type_scope *)

(* So (not A) is really a function that takes A and makes False *)

(* This makes for more interesting proof terms. For the next theorem,
    the goal is really
      forall A : Prof, A -> (~ A) -> False
    that is
      forall A : Prof, A -> (A->False) -> False
 
   So the proof is simple: if we have A and A->False, we can make a False:
 *)

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

Check notnot.
(* notnot
     : forall A : Prop, A -> ~ ~ A *)

(* OK, but what if we get both A and ~A? Well, we can make _anything_ at all.
    This is consistent with classic logic: from False anything follows. This is
     why False has no _constructors_ whatsoever, just the type definition that
     cannot get inhabited/populated. *)  

(* The following may feel like cheating: *)

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

Check abs.
(* abs
     : forall A C : Prop, A -> ~ A -> C *)
(* abs
     : forall A C : Prop, A -> ~ A -> C *)

(* Here's why it works: False has no constructors, so "match False" always succeeds.
    Rocq accepts it as proof of whatever type C follows.
   We can be more explicit about wanting C, syntactically, with an explicit "return".
    Because the match for False is empty, C is always returned.  *)


(* Example from the Harvard tutorial: *)

(* 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. 
 *)   

Theorem pqr': forall P Q R : Prop, (P -> (Q->R)) -> P/\Q -> R.
(*  *)
Proof (fun P Q R p2qr '(conj p q) => (p2qr p) q).
(* pqr' is defined *)

Check pqr'.
(* pqr'
     : forall P Q R : Prop, (P -> Q -> R) -> P /\ Q -> R *)

(* Distributivity example:  \/ is like addition , /\ is like multiplication  *)

Theorem and_or_distr : forall A B C : Prop, A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
(*  *)
Proof (fun A B C abc => match abc with conj a bc  => 
           match bc with 
            | or_introl b => or_introl (conj a b )
            | or_intror c => or_intror (conj a c )
           end 
         end).
(* and_or_distr is defined *)

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

(* Note that in the above /\ has higher syntactic precedence, so it's (A /\ B) \/ (A /\ C) in the goal. *)

(* An easier syntax, remembering that /\ is just a conj and only the conj *)

Theorem and_or_distr'' : forall A B C : Prop, A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
(*  *)
Proof (fun A B C '(conj a bc) => match bc with
            | or_introl b => or_introl (conj a b )
            | or_intror c => or_intror (conj a c )
           end).
           
(* and_or_distr'' is defined *)
            
(********* To be continued **********)