(* week-04_the-exists-tactic.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 07 Feb 2025 *)

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

(* Paraphernalia: *)

Require Import Arith.

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

Lemma proving_an_existential_example_0 :
  exists n : nat,
    n = 0.
Proof.
  exists 0.
  reflexivity.
Qed.

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

Lemma proving_an_existential_example_1 :
  forall n : nat,
  exists m : nat,
    S m = n + 1.
Proof.
  intro n.
  exists n.
  Search (_ + S _).
  Check (plus_n_Sm n 0).
  rewrite <- (plus_n_Sm n 0).
  Check Nat.add_0_r.
  rewrite -> (Nat.add_0_r n).
  reflexivity.
Qed.

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

Lemma proving_an_existential_example_2 :
  forall n : nat,
  exists f : nat -> nat,
    f n = n + 1.
Proof.
  intro n.
  exists S.
  rewrite <- (plus_n_Sm n 0).
  rewrite -> (Nat.add_0_r n).
  reflexivity.

  Restart.

  intro n.
  exists (fun n => S n).
  rewrite <- (plus_n_Sm n 0).
  rewrite -> (Nat.add_0_r n).
  reflexivity.

  Restart.

  intro n.
  exists (fun n => n + 1).
  reflexivity.
Qed.

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

(* end of week-04_the-exists-tactic.v *)