(* ###################################################################### *)
(** Questionable consequences of excluded middle or,
    equivalently, double negation elimination *)

Definition PEM := forall P: Prop, P \/ ~P.

Lemma nn_pem : forall P, ~~ (P \/ ~P).
Proof.
Admitted.

Lemma pem_nn : PEM -> forall P, ~~P -> P.
Proof.
Admitted.

(** Prove the following goals directly, without using nn_pem or pem_nn *)
Lemma p_or_p_impl_q : PEM -> forall (P Q: Prop), P \/ (P -> Q).
Proof.
Admitted.

Lemma nn_p_or_p_impl_q : forall (P Q: Prop), ~~(P \/ (P -> Q)).
Proof.
Admitted.

Lemma pq_or_qp : PEM -> forall (P Q: Prop), (P -> Q) \/ (Q -> P).
Proof.
Admitted.

Lemma nn_pq_or_qp : forall (P Q: Prop), ~~ ((P -> Q) \/ (Q -> P)).
Proof.
Admitted.

Definition even_ex (n: nat) := exists x, x+x = n.
Definition odd_ex (n: nat) := exists x, S(x+x) = n.


(** Easy *)
Lemma cheat_even_or_not : PEM -> forall n, even_ex n \/ ~ even_ex n.
Proof.
Admitted.

(** A much more informative proof is proposed below. 
    However we need new tactics for reasoning on constructors:
    tactics [discriminate] and [injection].
    The principles behind these tactics are explained below,
    first let us just use them. 
*)

(** Helper. Hint: use [plus_n_Sm] from the library *)
Theorem even_or_odd : forall n, even_ex n \/ odd_ex n.
Proof.
Admitted.

(** Note the advanced usage of [intros] *)
Lemma o_ne : forall n, odd_ex n -> ~(even_ex n).
intros n [p pp1] [q qq]. rewrite <- qq in pp1. clear n qq.
(** At this stage a strong enough induction has to be performed:
    hence the use of [revert], a converse of [intro] *)
revert q pp1; induction p as [ | p IHp]; destruct q as [ | q].
  - discriminate.
  - injection.  rewrite <- plus_n_Sm. discriminate.
  - (* FILL HERE *) admit.
  - (* FILL HERE *) admit.
Admitted.
  
Theorem even_or_not : forall n, even_ex n \/ ~ even_ex n.
Proof.
Admitted.


(* ###################################################################### *)
Lemma other_False : False <-> (forall X: Prop, X).
Proof.
split.
  intros F X. case F. 
  intro allX. exact (allX False).
Qed.

(* ###################################################################### *)

(** Constructors such as S are injective *)

Lemma S_inj : forall n m, S n = S m -> n = m.
Proof.
intros n m e.
(** The only way to use e is to rewrite it.
    To this effect, the trick is to replace n by an expression of (S n).
    Use the tactics [change] as follows: change n with (XXX).
    where XXX is a suitable expression of [S n] reducible to n.
    You can use the function [pred]. Perform Print pred to look
    at its definition. Then complete the proof. *)
Admitted.

(* The same proof can be performed using an automated tactics *)
Lemma S_inj_auto : forall n m, S n = S m -> n = m.
Proof.
intros n m e. injection e. intro; assumption.
Qed.


(* ###################################################################### *)
(** How to discriminate values built with different constructors *)

(** Propagation of confusion *)

(** Confusing the 2 Boolean constructors *)
Definition f1 (b: bool) : nat :=
  match b with
  | true => 4
  | false => 2
  end.

(** New tactic: 'change' [conclusion']
   which replaces the current conclusion with a
   computationally equal formula.
   Already known tactics such as 'simpl', 'red', 'unfold
   are actually special cases of 'change'.
*)
Lemma tf_confusing : true = false -> 4 = 2.
Proof.
intro e. change (f1 true = f1 false). rewrite e. reflexivity.
Qed.

(** The following does not work, as expected *)
Lemma tt_confusing : true = true -> 4 = 2.
Proof.
intro e. change 4 with (f1 true). try rewrite e. 
(* no effect *)
Abort.

(** Generalization *)
Definition g1 (A:Type) (x y: A) (b: bool) : A :=
  match b with
  | true => x
  | false => y
  end.

(** If [true = false], all values collapse in any type *)
Lemma gtf_confusing : true = false -> 
  forall A: Type, forall x y: A, x = y.
Proof.
intros e A x y. change (g1 A x y true = g1 A x y false).
rewrite e. reflexivity.
Qed.

(** Confusing 0 and successors *)
Definition f2 (n: nat) : nat :=
  match n with
  | O   => 4
  | S n => 2
  end.

Lemma O1_confusing : O = 1 -> 4 = 2.
Proof.
intro e. change (f2 O = f2 1). rewrite <- e. reflexivity.
Qed.

(* Exercise: state and prove that if 23 = 55, 
   then all values collapse in any type 
*)

(* FILL HERE *)

(* ------------------------------------------------------------ *)

(** Discriminating constructors *)
(** Constructors with distinguishable names, say C1 and C2,
   make different values, i.e., ~ (C1 params1 = C2 params2),
   that is, C1 params1 = C2 params2 -> False.
   This amounts to propagate confusion at the level of Prop,
   namely, to confuse False with a provable proposition,
   e.g. true = true, or the simplest one which is called True.
*)

Print True.

(** Discriminating natural numbers *)

(** Version 1 *)
Definition g3 (n: nat) : Prop :=
  match n with
  | 0 => False
  | S n => true = true
  end.

(** Version 2 *)
Definition g4 (n: nat) : Prop :=
  match n with
  | 0 => False
  | S n => True
  end.

Lemma O1_impossible_g3 : O = 1 -> False.
Proof.
intro e. change (g3 0). rewrite e.
unfold g3. reflexivity.
Qed.

Lemma O1_impossible_g4 : O = 1 -> False.
Proof.
intro e. change (g4 0). rewrite e.
unfold g4. apply I.
Qed.

(** The above trick is used by the Coq tactic called 'discriminate' *) 
Lemma O1_impossible_disc : O = 1 -> False.
Proof.
intro e. discriminate e.
Qed.

(** The tactic 'discriminate' can be used whatever the conclusion *)
Lemma tf_impossible_any_conclusion : true = false -> 10 <= 87.
Proof.
intro e. discriminate e.
Qed.

(* ------------------------------------------------------------ *)


(* ###################################################################### *)
(** Additional variations on False --  5 STARS *)

Inductive another_False : Prop :=
  AF: another_False -> another_False.

Inductive wrongnat : Set :=
  Swn : wrongnat -> wrongnat.

Lemma no_wrongnat : wrongnat -> False.
Admitted.

Lemma another_False_False : another_False -> False.
Admitted.



(** A way to discriminate natural numbers *)

Fixpoint nat_Peq (n m: nat) : Prop :=
  match n, m with
  | O, O => True
  | S n, S m => nat_Peq n m
  | _, _ => False
  end.

Theorem eq_nat_Peq : forall n m, n = m -> nat_Peq n m.
Proof.
Admitted. 
(* Use Defined rather than Qed here *)

(* Practical applications *)
Lemma t_3_5 : 3 = 5 -> False.
Proof. (* use eq_nat_Peq here *)
Admitted.
(* Use Defined rather than Qed here *)

Lemma t_3_5_disc : 3 = 5 -> False.
Proof.
intro e. discriminate e.
Defined.


(* Now the following two commands should provide the same 
   (or very similar) answers. 
*)
Eval compute in t_3_5.
Print t_3_5_disc.
 
(** Converse of eq_nat_Peq : 5 STARS  *) 
Theorem nat_Peq_correct : forall n m, nat_Peq n m -> n = m.
Proof.
Admitted.