(* week-03_the-revert-tactic.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 31 Jan 2025 *)

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

Lemma a_proposition_implies_itself :
  forall A : Prop,
    A -> A.
Proof.
  intro A.
  intro H_A.
  exact H_A.

  Restart.

  intro A.
  intro H_A.
  revert H_A.    (* <-- *)
  revert A.      (* <-- *)
  intros A H_A.
  exact H_A.
Qed.

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

Lemma swapping_the_order_of_quantifiers :
  forall A B : Prop,
    (A -> B -> A /\ B) -> B -> A -> A /\ B.
Proof.
  intros A B H_implication H_B H_A.
  exact (H_implication H_A H_B).

  Restart.

  intros A B H_implication H_B H_A.
  revert H_B.
  revert H_A.
  exact H_implication.

  Restart.

  intros A B H_implication H_B H_A.
  revert H_B.
  revert H_A.
  revert H_implication.
  exact (a_proposition_implies_itself (A -> B -> A /\ B)).

  Restart.

  intros A B H_implication H_B H_A.
  revert H_A H_B.
  exact H_implication.

  Restart.

  intros A B H_implication H_B H_A.
  revert H_implication H_A H_B.
  exact (a_proposition_implies_itself (A -> B -> A /\ B)).
Qed.

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

(* end of week-03_the-revert-tactic.v *)