(* 
destruct: Case analysis only. Split into cases and prove each one separately. 

induction: Case analysis + induction hypotheses
Split into cases and assume the statement holds for recursive subparts.
*)

Theorem plus_0_r : forall n, 0 + n = n.
Proof.
  intros.
  destruct n.
  - reflexivity. 
  - simpl. reflexivity. 
Qed.


Theorem plus_n_0 : forall n, n + 0 = n.
Proof.
  intros.
  induction n.
  - reflexivity. 
  - simpl.
  rewrite -> IHn. reflexivity.
Qed.

(*
discriminate: Constructor inequality. Two different constructors cannot be equal.
Use it when: These shapes can’t be equal.

contradiction: Logical inconsistency. use it when: Your assumptions 
contradict each other. You already assumed P and ¬ P (or equivalent).

*)

Theorem ex100: 0 = S 0 -> False.
Proof.
  intros. discriminate.
Qed.


Inductive color := Red | Blue.

Theorem ex101: Red = Blue -> False.
Proof.
  intros. discriminate.
Qed.

Theorem ex102: forall P : Prop, P -> ~P -> False.
Proof.
  intros. 
  (*unfold not in H0.
  apply H0 in H. assumption.  *)
  (*info_auto.*)
  contradiction.
Qed.

Theorem ex103: False -> 1=100.
Proof.
  intros.
  contradiction.
Qed.  
  

(* When contradiction works but discriminate does not*)
Theorem ex104 :forall P Q : 
   Prop, P -> (P -> False) -> Q.
Proof.
  intros. apply H0 in H. contradiction.
Qed.


(* When discriminate works but contradiction does not *)
Theorem ex105: S 0 = 0 -> False.
Proof.
  intros. discriminate.
Qed.

(* auto is a backward proof search tactic using a hint database:
It tries:

applying hypotheses
chaining implications
using constructors
resolving False goals *)

Goal forall P Q,
  P ->
  (P -> Q) ->
  (Q -> False) ->
  False.
Proof.
  intros. auto.
Qed.

(* unfold *)
From Stdlib Require Import Arith Nat Lia Ring.

Definition double (n : nat) := n + n.
Goal forall n, double (S n) = S (S (n + n)).
Proof.
  intros. unfold double.
  simpl. f_equal. rewrite Nat.add_comm. simpl. reflexivity.
Qed.
  

Goal double 3 = 6.
Proof. 
    unfold double. simpl. reflexivity.  
Qed.

Goal forall n, double n = n + n.
Proof.
  intros.
  unfold double.
  reflexivity.
Qed. 

(* rewrite vs apply *)

Goal forall n, 0 + n = n.
Proof.   
  intros. 
  Check plus_O_n.
  (* apply plus_O_n.*)
  rewrite plus_O_n. reflexivity.
Qed.

(* f_equal vs injection *)
Goal forall x y, x = y->S x = S y.
Proof.  
  intros.
  f_equal. 
  assumption.
Qed.

Goal forall x y, S x = S y -> x = y.
Proof.
  intros. injection H as H2. assumption.
Qed.