(* week-07_the-situation-so-far.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 07 Mar 2025 *)

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

Require Import Arith Bool List.

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

Proposition clearly :
  forall A B : Prop,
    A -> B -> A.
Proof.
  intros A B H_A H_B.
  clear H_B.
  exact H_A.
Qed.

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

Proposition true_or_false :
  forall b : bool,
    b = true \/ b = false.
Proof.
  intro b.
  case b as [ | ] eqn:H_b.
  - left.
    reflexivity.
  - right.
    reflexivity.
Qed.

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

Proposition reflexivity_of_implication :
  forall A : Prop,
    A -> A.
Proof.
  intros A H_A.
  exact H_A.
Qed.

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

Proposition zero_is_not_one :
  0 <> 1.
Proof.
  unfold not.
  (* the goal is now: 0 = 1 -> False *)
  intro H_absurd.
  discriminate H_absurd.
Qed.

Proposition nil_is_not_cons :
  forall (V : Type)
         (v : V),
  nil <> v :: nil.
Proof.
  intros V v.
  unfold not.
  intro H_absurd.
  discriminate H_absurd.
Qed.

(* ***** *)

Proposition a_list_is_not_another_list :
  forall (n1 n2 : nat),
    n1 :: 2 :: n2 :: nil <> 1 :: n2 :: 3 :: nil.
Proof.
  intros n1 n2.
  unfold not.
  intro H_tmp.
  injection H_tmp as eq_n1_1 eq_2_n2 eq_n2_3.
  rewrite <- eq_2_n2 in eq_n2_3.
  discriminate eq_n2_3.
Qed.

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

Proposition even_or_odd :
  forall n : nat,
    (exists q : nat,
        n = 2 * q)
    \/
    (exists q : nat,
        n = S (2 * q)).
Proof.
  intro n.
  induction n as [ | n' [[q IHq] | [q IHq]]].
  - left.
    exists 0.
    exact (eq_sym (Nat.mul_0_l 2)).
  - rewrite -> IHq.
    right.
    exists q.
    reflexivity.
  - rewrite -> IHq.
    left.
    exists (S q).
    Search (_ * S _ = _ + _).
    rewrite -> (Nat.mul_succ_r 2 q).
    rewrite <- (plus_n_Sm (2 * q) 1).
    rewrite -> (Nat.add_1_r (2 * q)).
    reflexivity.
Qed.

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

Proposition this_one :
  forall (V : Type)
         (v1 v2 : V),
    (v1, v2) <> (v2, v1).
Proof.
Abort.

Proposition that_one :
  exists (V : Type)
         (v1 v2 : V),
    (v1, v2) <> (v2, v1).
Proof.
Abort.

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

(* end of week-07_the-situation-so-far.v *)