(* Basic solution *)
Lemma remove_S: forall x y, S x= S y -> x = y.
Proof.
intros x y e.
Print pred.
change x with (pred (S x)). 
rewrite e. reflexivity.
Qed.


(* Inventing an appropriate projection online *)
Lemma remove_S2: forall x y, S x= S y -> x = y.
Proof.
intros x y e.
pose (f n := match n with S z => z | _ => x end).
change x with (f (S x)). 
rewrite e. simpl. reflexivity.
Qed.

(* On lists *)
Require Import List.

Lemma remove_cons2:
  forall (A: Type) (x y: A) (u v: list A), x :: u = y :: v -> u = v.
Proof.
intros A x y u v e.
(* Note: tl does not need to have an argument for A *)
pose (tl (l: list A) := match l with nil => nil | a :: l' => l' end).
change u with (tl (x :: u)). rewrite e. reflexivity.
Qed.

Definition general_tl (A: Type) (l: list A) := 
  match l with nil => nil | a :: l' => l' end.

(* Issue : the head (of a list) is a partial function:
   undefined if A is empty *)
(*
Definition general_head (A: Type) (l: list A) := 
  match l with nil => ??? | a :: l' => a end.
*)

Lemma remove_cons1:
  forall (A: Type) (x y: A) (u v: list A), x :: u = y :: v -> x = y.
Proof.
intros A x y u v e.
injection e. intros; assumption.
Show Proof.
Qed.

Lemma remove_cons1_automatic :
  forall (A: Type) (x y: A) (u v: list A), x :: u = y :: v -> x = y.
Proof.
intros A x y u v e. (* Yes I'm rich ! x is in A *)
(* Note: tl does not need to have an argument for A *)
pose (hd (l: list A) := match l with nil => x | a :: l' => a end).
change x with (hd (x :: u)). rewrite e. simpl. reflexivity.
Qed.


Inductive even : nat -> Prop := 
  | E0 : even 0
  | E2 : forall n, even n -> even (S (S n)).

Section sec_invert_even.
Variable f: nat -> Prop.
Hypothesis f0 : f 0.
Hypothesis f2: forall n, even n -> f (S (S n)).

Definition even_f: forall n, even n -> f n.
Proof.
intros n e. destruct e. Show Proof.
  exact f0. 
  exact (f2 n e).
Defined.

End sec_invert_even.

Lemma invert_even : 
  forall n, even n -> n = 0 \/ exists x, (even x /\ n = S (S x)).
Proof.
intros n e. destruct e as [ | m em].
  left. reflexivity.
  right. exists m. split; trivial. 
Qed.

Lemma no_even_1: even 1 -> False.
Proof.
intros e. (* destruct e. (* stuck here*) Undo.  *)
generalize (invert_even 1 e). intros [ e10 | [x [evx e1SSx]]].
  discriminate e10.
  discriminate e1SSx. 
Qed.

Lemma no_even_1_other_tactic : even 1 -> False.
Proof.
intros e. 
destruct (invert_even 1 e) as [ e' | [x [evx e']]]; discriminate e'.
Qed.


Lemma no_even_1_clever: even 1 -> False.
Proof.
intros e.
pose (f n := match n with 1 => False | _ => True end).
change (f 1). destruct e; exact I. Show Proof.
Qed.


Lemma no_even_1_convenient: even 1 -> False.
Proof.
intros e. inversion e. (* Show Proof. *)
Qed.


Lemma even_minus2: forall n, even (S (S n)) -> even n.
Proof.
intros n e. 
destruct (invert_even _ e) as [ e' | [x [evx e']]]. 
  discriminate e'. 
  injection e'. intro enx. rewrite enx. assumption.
Qed.


Lemma even_minus2_convenient: forall n, even (S (S n)) -> even n.
Proof.
intros n e. inversion e. 
(*exact H0 bad policy: depnds on names chosen by coq . *)
assumption.
Qed.


Lemma even_minus2_convenient': forall n, even (S (S n)) -> even n.
Proof.
intros n e. inversion e as [ | n0 even_n dontcare].
(*exact H0 bad policy: depnds on names chosen by coq . *)
exact even_n.
Qed.

Print even_minus2_convenient'.


(* Partial functions *)

Section sec_pf.
Variable A B: Type.

(* partial f : A -> B *)

(* First way *)
Print option.

(*
Inductive option (A : Type) : Type :=
 | Some : A -> option A
 | None : option A

like a list with either 0 or exactly 1 element
*)
Definition f: A -> option B.
(* some body *)
Admitted.

(* Usage: 
  - when [f x] is defined, return [Some (f x)]
  - otherwose, return None
*)

(* Second way *)
(* Assuming a defindness predicate P *)
Variable P : A -> Prop.
Definition f': forall x:A, P x -> B.
intros x p. 
(* analyze x; impossible values will be combined with p : P x
   to get a False assumption which can be eliminated
*)


(* Third way see find_mind *)