(* week-04_backward-and-forward-proofs.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 09 Feb 2024 *)

(* ***********)

(* Learning goals:

   * using apply among the assumptions

   * using assert to declare a new assumption

   * using split to prove conjunctions
*)

(* ***********)

Proposition identity :
  forall A : Prop,
    A -> A.
Proof.
  intros A H_A.
  apply H_A.
Qed.

Proposition modus_ponens :
  forall A B : Prop,
    A -> (A -> B) -> B.
Proof.
  intros A B H_A H_A_implies_B.
  (* backward, from the goal: *)
  apply H_A_implies_B.
  apply H_A.

  Restart.

  intros A B H_A H_A_implies_B.
  (* forward, from the initial hypothesis: *)
  apply H_A_implies_B in H_A.
  exact H_A.

  Restart.

  intros A B H_A H_A_implies_B.
  (* forward, keeping in control of the naming: *)
  assert (H_B := H_A_implies_B H_A).
  exact H_B.
Qed.

Proposition modus_ponens_and_more :
  forall A B C : Prop,
    A -> (A -> B) -> (B -> C) -> C.
Proof.
  intros A B C H_A H_A_implies_B H_B_implies_C.
  (* backward, from the goal: *)
  apply H_B_implies_C.
  apply H_A_implies_B.
  apply H_A.

  Restart.

  intros A B C H_A H_A_implies_B H_B_implies_C.
  (* forward, from the initial hypothesis: *)
  Check (H_A_implies_B H_A).
  assert (H_B := H_A_implies_B H_A).
  Check (H_B_implies_C H_B).
  exact (H_B_implies_C H_B).
Qed.

Proposition modus_ponens_and_even_more :
  forall A B C D : Prop,
    A -> (A -> B) -> (B -> C) -> (C -> D) -> D.
Proof.
  intros A B C D H_A H_A_implies_B H_B_implies_C H_C_implies_D.
  (* backward, from the goal: *)
  apply H_C_implies_D.
  apply H_B_implies_C.
  apply H_A_implies_B.
  apply H_A.

  Restart.

  intros A B C D H_A H_A_implies_B H_B_implies_C H_C_implies_D.
  (* forward, from the initial hypothesis: *)
  assert (H_B := H_A_implies_B H_A).
  assert (H_C := H_B_implies_C H_B).
  Check (H_C_implies_D H_C).
  exact (H_C_implies_D H_C).
Qed.

(* ********** *)

(* Prove foo:

   (1) backward, in a goal-directed way

   (2) forward, from the assumptions
*)

Proposition foo :
  forall P Q R1 R2 : Prop,
    P -> (P -> Q) -> (Q -> R1) /\ (Q -> R2) -> R1 /\ R2.
Proof.
Abort.

(* ********** *)

(* Prove bar:

   (1) by using the split tactic as early as possible 

   (2) by using the split tactic as late as possible 
*)

Proposition bar :
  forall P1 P2 Q R1 R2 T1 T2 : Prop,
    P1 -> (P1 -> P2) -> (P2 -> Q) -> (Q -> R1) -> (R1 -> T1) -> (Q -> R2) -> (R2 -> T2) -> T1 /\ T2.
Proof.
  intros P1 P2 Q R1 R2 T1 T2.
  intros H_P1 H_P1_implies_P2 H_P2_implies_Q H_Q_implies_R1 H_R1_implies_T1 H_Q_implies_R2 H_R2_implies_T2.

  (* Here, use the split tactic as early as possible. *)

  Restart.

  intros P1 P2 Q R1 R2 T1 T2.
  intros H_P1 H_P1_implies_P2 H_P2_implies_Q H_Q_implies_R1 H_R1_implies_T1 H_Q_implies_R2 H_R2_implies_T2.

  (* Here, use the split tactic as late as possible. *)

Abort.

(* ********** *)

(* Prove baz:

   (1) by using the split tactic as early as possible 

   (2) by using the split tactic as late as possible 
*)

Proposition baz :
  forall P Q R T U1 U2 : Prop,
    P -> (P -> Q) -> (Q -> R) -> (R -> T) -> (T -> U1) -> (T -> U2) -> U1 /\ U2.
Proof.
  intros P Q R T U1 U2.
  intros H_P H_P_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U1 H_T_implies_U2.

  (* Here, use the split tactic as early as possible. *)

  Restart.

  intros P Q R T U1 U2.
  intros H_P H_P_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U1 H_T_implies_U2.

  (* Here, use the split tactic as late as possible. *)

Abort.

(* ********** *)

(* Complete the proofs of baz_dual,
   and then compare them.
*)

Proposition baz_dual_early :
  forall P1 P2 Q R T U : Prop,
    (P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U.
Proof.
  intros P1 P2 Q R T U.
  intros H_P1_or_P2 H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U.

  (* use "destruct H_P1_or_P2 as [H_P1 | H_P2]." as early as you can *)

Abort.

Proposition baz_dual_late :
  forall P1 P2 Q R T U : Prop,
    (P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U.
Proof.
  intros P1 P2 Q R T U.
  intros H_P1_or_P2 H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U.

  (* use "destruct H_P1_or_P2 as [H_P1 | H_P2]." as late as you can *)

Abort.

(* Complete the following proof.
   What do you end up with?
   A proof close to that of Proposition baz_dual_early,
   or to that of Proposition baz_dual_late?
   What do you conclude?
*)
Proposition baz_dual_early_or_late :
  forall P1 P2 Q R T U : Prop,
    (P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U.
Proof.
  intros P1 P2 Q R T U.
  intros [H_P1 | H_P2] H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U.

Abort.

(* ********** *)

(* How would you prove the following propositions?
   Forward or backward?
*)

Proposition ladidah :
  forall P1 P2 P3 P4 Q R T U : Prop,
    (P1 \/ P2) \/ (P3 \/ P4) -> (P1 -> Q) -> (P2 -> Q) -> (P3 -> Q) -> (P4 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U.
Abort.

Proposition toodeloo :
  forall P Q R T U1 U2 U3 U4: Prop,
    P -> (P -> Q) -> (Q -> R) -> (R -> T) -> (T -> U1) -> (T -> U2) -> (T -> U3) -> (T -> U4) -> (U1 /\ U2) /\ (U3 /\ U4).
Abort.

(* How complex could the size of such proofs be
   (relative to the number of hypotheses about P1, P2, P3, etc.
   and to the number of conclusions about U1, U2, U3, etc.)?
*)

(* ***********)

(* end of week-04_backward-and-forward-proofs.v *)
