(* All experiments with the ssreflect library must start with a loading a few files and setting
   a few notational conventions.  To know which files to load, use the "API" link in the
   coqlive documentation, or browse the page
      http://coqfinitgroup.gforge.inria.fr/ssreflect-1.3/
*)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* The following command can be used to check that an expression is well-formed. *)

Check 1.

(* The following command would fail.

Check 1 + (1,2).

*)

(* You describe a function by writing fun .. => .. 
  The following is a function from nat to nat.
  Describing a function does not define anything. *)

Check fun x : nat => 3 + x + x.

(* To define a new object, use the keyword definition. *)

Definition add3_and_double : nat -> nat :=  fun x => 3 + x + x.

(* When A and B are propositions, A -> B should be read as "A implies B".
   A proposition is also a type, and any element of that type is also a 
   proof of that proposition.  Here is a proof of for every properties A and B,
   A implies that B implies A. *)

Check (fun A B : Prop => fun (x : A) (y : B) => y).

(* False propositions can be written, they are propositions without proofs,
   empty types. *)

(* Beware of discrepancy between defined objects and mathematical customs.
   For instance, it is customary to avoid talking about 2 - 3 as an operation
   between natural numbers.  In Coq it is well defined and equals 0. *)

Compute 2 - 3.

(* Families of types. seq is not a type, but a family of types, indexed by
   types.  Thus, seq nat is a type (the type of sequences of natural numbers)
   and seq bool is another type, in the same family. *)

Check seq.

(* Some function can return outputs in a variety of types, all members
   of a famility.  The notation for the type of these functions uses the
   forall identifier. *)
Check nseq.

Compute nseq 3 true.

Compute nseq 3 1.

(* 3 is a notation that hides some particular structure, built only with
   S and O. *)

Check S (S (S O)).

(* Many binary notations are provided. *)

Check true && false.

Check fun x : nat => true.

Compute fun x => 2 < 5 + x.

(* Implicit arguments: a strategy to reduce the amount of redundant information
   that a user must write.

   Normally nseq has 3 arguments: a type T, a natural number, and an element
   of type T, that will be repeated in the result.  But when we use nseq, we
   write only 2 arguments.  The value of the first can be guessed from the type
   of the third.  So we only give the second and the third. *)

Check nseq.

Check nseq 1 true.

Compute nseq 1 true.

(* Same with cat, but difficult to ask for its type.  the command
   Check cat  fails. *)
Check @cat.

Compute cat [:: 1; 2] [:: 3; 4].

(* Coercions: added when there is a natural way to see some value as an
   element of another type. *)

Compute (true : nat).

(* The existence of coercions makes types surprising, sometimes. *)

Check 1 + true.

(* Asserting that some type may have a certain characteristic.  For instance,
   it is important to know when there exists a boolean function to compare
   elements for equality in a given type. *)

Print eqType.
Print Equality.type.

Print nat.
Print nat_eqType.
Print Canonical Projections.
Check eq_sym.

Lemma try_eq_sym : (3 == 1) = (1 == 3).
apply : eq_sym.
Qed.

Search cancel.

Lemma sum_3_power4 : forall a b c, a ^ 4 + b ^ 4 + c ^ 4 <= (a + b + c) ^ 4.
Proof.
have expn_convex : forall a b n, a ^ n.+1 + b ^ n.+1 <= (a + b) ^ n.+1.
  move => a b; elim => [ | n IHn].
(* Here we have three subgoals, the indentation is 4 = 2 * (3 - 1) *)
    by rewrite leqnn.
(* The last tactic solved the goal, it is marked with "by". *)
  rewrite [(a + b) ^ _]expnS.
  rewrite (leq_trans (_ : _ <= (a + b) * (a ^ n.+1 + b ^ n.+1))) //.
(* Now we have three goals again. *)
    rewrite muln_addr !muln_addl [a * b ^ _ + _]addnC addnAC !expnS -!addnA.
    by rewrite leq_add // leq_addr.
  by apply: leq_mul.
move => a b c; apply: (leq_trans _ (expn_convex _ _ _)).
by apply: leq_add.
Qed.

Search (_ * _ <= _ * _).

Search (_ = _) (_ * _).

Search (_ = _) (_ * _) (_ <= _).