Section inconsistent.
Variable P Q: Prop.


Hypothesis h1: P -> Q.
Hypothesis h2: Q -> False.
Hypothesis h3: P.


Theorem WHAT: False.
auto.
Qed.

End inconsistent.


Section sec.

Variable P: Prop.

Lemma lem1: P -> P.
Proof.
(* Maths : "let us assume P" *)
(* Coq : "let us assume x: P" *)
intros x.
exact x.
Show Proof.
Qed.


Lemma lem2_left : P -> P -> P.
Proof.
intros x y.
exact x.
Defined.

Lemma lem2_right : P -> P -> P.
Proof.
intros x y.
exact y.
Defined.

Compute (lem2_left,lem2_right).

(* 
Note the difference between
- Qed: we are not interested in the contents
- Defined: we ARE interested in the contents, and want to compute with it.
*)


Definition idn: nat -> nat.
exact (fun x => x).
Qed.

Compute idn.

End sec.

(* Querying information *)

About "\/".
Print or.

About "/\".
Print and.

(*

Inductive and (A B : Prop) : Prop :=  
  conj : A -> B -> A /\ B

*)

Print prod.

(*
Inductive prod (A B : Type) : Type :=  
  pair : A -> B -> A * B

*)

(* "*" can be understood as prod *)

Compute (2,false) : prod nat bool.

(* "*" can be understood as mult *)
Compute 2 * 3.

Section sec2.
Variables A B: Set.

Definition comm : A * B -> B * A.
intros p. destruct p as [x y].
  split. 
    exact y.
    exact x.
(*
exact (fun p => match p with
          (x,y) => (y,x) end).

*)
Defined.

Print comm.

End sec2.

Section sec3.
Variables P Q: Prop.

Definition and_comm : P /\ Q -> Q /\ P.
Proof.
intros p. destruct p as [x y].
  split. 
    exact y.
    exact x.
Defined.

Compute and_comm.

End sec3.

Print comm.

Compute (comm nat bool (2,false)).

Compute (comm _ _ (2,false)).

(* About implicit arguments *)
Definition comm' {A B: Set} (p: A*B) := 
  comm A B p.

Compute (comm' (2,false)).

Print comm'.
Print and.

Inductive P248 : nat -> Prop :=
  | is2 : P248 2
  | is4 : P248 4
  | is8 : P248 8.

Fixpoint even (n: nat) : Prop :=
  match n with 
  | O => True
  | 1 => False
  | S (S n') => even n'
  end.

Lemma P248_even : 
  forall n, P248 n -> even n.
Proof.
intros n p248_n.
destruct p248_n; simpl; exact I.
Qed.

Lemma P248__not1 : P248 1 -> False.
Proof.
intros p. (* destruct p wont work *)
change (even 1). 
apply P248_even. assumption.
Qed.

(* The following theorem requires an arbitrary
   number of destruct, hence the fixpoint *)
Fixpoint plus0 (n:nat) :
   n + 0 = n.
Proof.
destruct n as [ | n1].
  reflexivity.
  simpl.
    pattern n1 at 2; case (plus0 n1). reflexivity.
Defined.

Print plus0.

Definition l5_basic: 5+0=5.
reflexivity.
Defined.

Compute l5_basic.

Definition l5: 5+0=5.
apply plus0.
Defined.

Compute l5.

Section sec_ind.
Variable P : nat -> Prop.
Hypothesis p0:  P O.
Hypothesis step: forall n, P n -> P (S n).

(* The induction principle is proved by fixpoint *)
Fixpoint nat_induction (n:nat) : P n.
Proof.
destruct n  as [ |n'].
  exact p0.
  apply step. apply (nat_induction n').
Qed.

End sec_ind.

(* Using our induction *)
Lemma plus0_other_proof: forall n: nat, n+0 = n.
Proof.
intro n. pattern n. apply nat_induction.
  reflexivity.
  intros n' e. simpl. rewrite e. reflexivity.
Qed.

(* Using standard induction *)
Lemma plus0_standard_proof: forall n: nat, n+0 = n.
Proof.
intro n. induction n as [| n' e].
  reflexivity.
  simpl. rewrite e. reflexivity.
Qed.