(* week-07_ex-falso-quodlibet.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 07 Mar 2025 *)

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

Require Import Arith.

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

Property foo :
  forall P : nat -> Prop,
    (exists i : nat,
        P i) ->
    forall j : nat,
      P j.
Proof.
Abort. (* does not hold, see just below *)

Theorem ex_falso_quodlibet_eg_False :
  (forall P : nat -> Prop,
      (exists i : nat,
          P i) ->
      forall j : nat,
        P j) ->
  0 = 1.
Proof.
  intro H_absurd.
  Check (H_absurd
           (fun n : nat => 0 = n)).
  (* : (exists i : nat, 0 = i) -> forall j : nat, 0 = j *)
  (* wanted: exists i : nat, 0 = i *)
  Check ex_intro.
  Check (ex_intro
           (fun i : nat => 0 = i)).
  (* : forall x : nat, 0 = x -> exists i : nat, 0 = i *)
  (* let's pick 0, for example *)
  Check (ex_intro
           (fun i : nat => 0 = i)
           0).
  Check (ex_intro
           (fun i : nat => 0 = i)
           0
           (eq_refl 0)).
  (* : exists i : nat, 0 = i *)
  (* which is what we wanted *)
  Check (H_absurd
           (fun n : nat => 0 = n)
           (ex_intro
              (fun i : nat => 0 = i)
              0
              (eq_refl 0))).
  (* : forall j : nat, 0 = j *)
  (* let's pick 1, for example *)
  Check (H_absurd
           (fun n : nat => 0 = n)
           (ex_intro
              (fun i : nat => 0 = i)
              0
              (eq_refl 0))
           1).
  (* : 0 = 1 *)
  exact (H_absurd
           (fun n : nat => 0 = n)
           (ex_intro
              (fun i : nat => 0 = i)
              0
              (eq_refl 0))
           1).
Qed.

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

Lemma truism :
  forall P : nat -> Prop,
    (exists n : nat,
        P n) ->
    exists n : nat,
      P n.
Proof.
  intros P H_P.
  Check ex_intro.
  Check (ex_intro
           P).
  destruct H_P as [n H_Pn].
  Check (ex_intro
           P
           n).
  Check (ex_intro
           P
           n
           H_Pn).
  exact (ex_intro
           P
           n
           H_Pn).
Qed.  

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

(* Exercise 12 *)

Proposition ex_falso_quodlibet_indeed :
  (forall (P : nat -> Prop),
      (exists i : nat,
          P i) ->
      forall j : nat,
        P j) -> False.
Proof.
Abort.

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

Property False_implies_anything :
  forall A : Prop,
    False -> A.
Proof.
  intros A F.
  contradiction F.
Qed.

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

(* Exercise 13 *)

Property foo : (* stated again, but admitted this time... *)
  forall P : nat -> Prop,
    (exists i : nat,
        P i) ->
    forall j : nat,
      P j.
Proof.
Admitted. (* ...to prove the following theorem as a corollary of foo *)

Theorem ex_falso_quodlibet_eg_True :
  forall m : nat,
    exists n : nat,
      m < n.
Proof.
  Check (foo (fun m : nat => exists n : nat, m < n)).
Abort.

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

(* Exercise 14 *)

Proposition an_equivalence :
  (forall P : nat -> Prop,
      (exists i : nat,
          P i) ->
      forall j : nat,
        P j)
  <->
  (forall (P : nat -> Prop)
          (i : nat),
      P i ->
      forall j : nat,
        P j).
Proof.
Admitted.

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

(* Exercise 15 *)

Property bar :
  forall (P : nat -> Prop)
         (i : nat),
    P i ->
    forall j : nat,
      P j.
Proof.
Abort. (* does not hold, see just below *)

Theorem ex_falso_quodlibet_eg_False_revisited :
  (forall (P : nat -> Prop)
          (i : nat),
      P i ->
      forall j : nat,
        P j) ->
  0 = 1.
Proof.
Abort.

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

(* Exercise 16 *)

Property bar : (* stated again, but admitted this time... *)
  forall (P : nat -> Prop)
         (i : nat),
    P i ->
    forall j : nat,
      P j.
Proof.
Admitted. (* ...to prove the following theorem as a corollary of bar *)

Theorem ex_falso_quodlibet_eg_True_revisited :
  forall m : nat,
    exists n : nat,
      m < n.
Proof.
  Check (bar (fun m : nat => exists n : nat, m < n)).
Abort.

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

(* end of week-07_ex-falso-quodlibet.v *)