Coq Proof: 0 = 1 -> 0 = 1 + n

different-solutions.v

(* https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html *)

Definition ex0 : 
  forall n : nat,
  0 = 1 -> 0 = 1 + n 
  := 
  fun n e1 => 
  nat_ind 
  (fun n => 0 = 1 + n) 
  e1 
  (fun _ s => 
    let e2 := f_equal S s in 
    eq_trans e1 e2
    )  n.

Definition ex1 : 
  forall n : nat,
  0 = 1 -> 0 = 1 + n 
  := 
  fix go n e1 :=
  match n with 
    | O => e1 
    | S n => 
      let e2 := f_equal S (go n e1) in 
      eq_trans e1 e2
  end.

Theorem ex2 : 
  forall n : nat,
  0 = 1 -> 0 = 1 + n. 
  Proof.
  intros.
  induction n.
  - discriminate.
  -  simpl. rewrite -> IHn.
     simpl. discriminate.
  Qed.

Definition ex3 : 
  forall n : nat,
  0 = 1 -> 0 = 1 + n 
  := 
  fun _ e => match e with end.


Theorem ex4 : 
  forall n : nat,
  0 = 1 -> 0 = 1 + n. 
  Proof.
  discriminate.
  Qed.

(* https://stackoverflow.com/questions/14644086/proving-p-q-q-p-using-coq-proof-assistant/ *)
Lemma contrapositive : 
  forall P : Prop,
  forall Q : Prop,
  (~Q -> ~P) -> P -> Q.
Admitted.


Definition ex5 :
  forall n : nat,
  0 = 1 -> 0 = 1 + n 
  :=
  fun n e1 => 
  let mot y := match y with | 0 => True | _ => False end in 
  let e2 := eq_ind 0 mot I 1 e1 in 
  contrapositive (0 = 1) (0 = 1 + n) (fun _ _ => e2) e1.