Merge branch 'v8.5'

1 files changed, 144 insertions, 70 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index b03aa64090..c8dd220baf 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -849,26 +849,41 @@ mapped to {\Prop}.
 
 Use some theorem or assumption or use the {\split} tactic.
 \begin{coq_example}
-Goal forall A B:Prop, A->B-> A/\B.
+Goal forall A B:Prop, A -> B -> A/\B.
 intros.
 split.
 assumption.
 assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{My goal contains a conjunction as an hypothesis, how can I use it?}
 
-If you want to decompose your hypothesis into other hypothesis you can use the {\decompose} tactic:
+If you want to decompose a hypothesis into several hypotheses, you can
+use the {\destruct} tactic:
 
 \begin{coq_example}
-Goal forall A B:Prop, A/\B-> B.
+Goal forall A B:Prop, A/\B -> B.
 intros.
-decompose [and] H.
+destruct H as [H1 H2].
 assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
+
+You can also perform the destruction at the time of introduction:
 
+\begin{coq_example}
+Goal forall A B:Prop, A/\B -> B.
+intros A B [H1 H2].
+assumption.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{My goal is a disjunction, how can I prove it?}
 
@@ -878,26 +893,28 @@ reasoning step, use the {\tt classic} axiom to prove the right part with the ass
 that the left part of the disjunction is false.
 
 \begin{coq_example}
-Goal forall A B:Prop, A-> A\/B.
+Goal forall A B:Prop, A -> A\/B.
 intros.
 left.
 assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 An example using classical reasoning:
 
 \begin{coq_example}
 Require Import Classical.
 
-Ltac classical_right := 
-match goal with 
-| _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right])
+Ltac classical_right :=
+match goal with
+| _:_ |- ?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right])
 end.
 
-Ltac classical_left := 
-match goal with 
-| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left])
+Ltac classical_left :=
+match goal with
+| _:_ |- _ \/ ?X1 => (elim (classic X1);intro;[right;trivial|left])
 end.
 
 
@@ -905,8 +922,10 @@ Goal forall A B:Prop, (~A -> B) -> A\/B.
 intros.
 classical_right.
 auto.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{My goal is an universally quantified statement, how can I prove it?}
 
@@ -935,8 +954,10 @@ Goal exists x:nat, forall y, x+y=y.
 exists 0.
 intros.
 auto.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{My goal is solvable by  some lemma, how can I prove it?}
@@ -954,8 +975,10 @@ Qed.
 
 Goal 3+0 = 3.
 apply mylemma.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 
@@ -972,8 +995,10 @@ Just use the {\reflexivity} tactic.
 Goal forall x, 0+x = x.
 intros.
 reflexivity.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{My goal is a {\tt let x := a in ...}, how can I prove it?}
 
@@ -987,13 +1012,21 @@ Just use the {\destruct} c as (a,...,b) tactic.
 
 \Question{My goal contains some existential hypotheses, how can I use it?}
 
-You can use the tactic {\elim} with you hypotheses as an argument.
-
-\Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses?}
+As with conjunctive hypotheses, you can use the {\destruct} tactic or
+the {\intros} tactic to decompose them into several hypotheses.
 
-\begin{verbatim}
-Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H.
-\end{verbatim}
+\begin{coq_example*}
+Require Import Arith.
+\end{coq_example*}
+\begin{coq_example}
+Goal forall x, (exists y, x * y = 1) -> x = 1.
+intros x [y H].
+apply mult_is_one in H.
+easy.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{My goal is an equality, how can I swap the left and right hand terms?}
@@ -1004,8 +1037,10 @@ Goal forall x y : nat, x=y -> y=x.
 intros.
 symmetry.
 assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{My hypothesis is an equality, how can I swap the left and right hand terms?}
 
@@ -1016,8 +1051,10 @@ Goal forall x y : nat, x=y -> y=x.
 intros.
 symmetry in H.
 assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{My goal is an equality, how can I prove it by transitivity?}
@@ -1029,8 +1066,10 @@ intros.
 transitivity y.
 assumption.
 assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{My goal would be solvable using {\tt apply;assumption} if it would not create meta-variables, how can I prove it?}
@@ -1066,7 +1105,6 @@ eapply trans.
 apply H.
 auto.
 Qed.
-
 \end{coq_example}
 
 \Question{My goal is solvable by  some lemma within a set of lemmas and I don't want to remember which one, how can I prove it?}
@@ -1103,8 +1141,10 @@ Use the {\assumption} tactic.
 Goal 1=1 -> 1=1.
 intro.
 assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?}
@@ -1114,8 +1154,10 @@ Use the {\exact} tactic.
 Goal 1=1 -> 1=1 -> 1=1.
 intros.
 exact H0.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{What can be the difference between applying one hypothesis or another in the context of the last question?}
 
@@ -1131,8 +1173,10 @@ Just use the {\tauto} tactic.
 Goal forall A B:Prop, A-> (A\/B) /\ A.
 intros.
 tauto.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{My goal is a first order formula, how can I prove it?}
 
@@ -1149,8 +1193,10 @@ Just use the {\congruence} tactic.
 Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a.
 intros.
 congruence.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it?}
@@ -1161,8 +1207,10 @@ Just use the {\congruence} tactic.
 Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b.
 intros.
 congruence.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it?}
@@ -1173,11 +1221,13 @@ Just use the {\ring} tactic.
 Require Import ZArith.
 Require Ring.
 Local Open Scope Z_scope.
-Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. 
+Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b.
 intros.
 ring.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{My goal is an equality on some field (e.g. real numbers), how can I prove it?}
 
@@ -1187,30 +1237,30 @@ Just use the {\field} tactic.
 Require Import Reals.
 Require Ring.
 Local Open Scope R_scope.
-Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. 
+Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1.
 intros.
 field.
-cut (b*a <>0 -> a<>0).
-cut (b*a <>0 -> b<>0).
-auto.
-auto with real.
-auto with real.
-Qed.
+split ; auto with real.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
-\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?}
+\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from $+$, $-$, constants, and variables), how can I prove it?}
 
 
 \begin{coq_example}
 Require Import ZArith.
 Require Omega.
 Local Open Scope Z_scope.
-Goal forall a : Z, a>0 -> a+a > a. 
+Goal forall a : Z, a>0 -> a+a > a.
 intros.
 omega.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?}
@@ -1233,16 +1283,22 @@ assert (A->C).
 intro;apply H0;apply H;assumption.
 apply H2.
 assumption.
+\end{coq_example}
+\begin{coq_example*}
 Qed.
+\end{coq_example*}
 
+\begin{coq_example}
 Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. 
 intros.
 cut (A->C).
 intro.
 apply H2;assumption.
 intro;apply H0;apply H;assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 
@@ -1333,8 +1389,10 @@ H1
 *)
 intros A B C H H0 H1.
 repeat split;assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{I want to automatize the use of some tactic, how can I do it?}
 
@@ -1347,8 +1405,10 @@ Goal forall A B C : Prop, A -> B/\C -> A/\B/\C.
 Proof with assumption.
 intros.
 split...
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{I want to execute the {\texttt proof with} tactic only if it solves the goal, how can I do it?}
 
@@ -1360,8 +1420,10 @@ Local Open Scope Z_scope.
 Goal forall a b c : Z, a+b=b+a.
 Proof with try solve [ring].
 intros...
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{How can I do the opposite of the {\intro} tactic?}
 
@@ -1373,8 +1435,10 @@ intros.
 generalize H.
 intro.
 auto.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it?}
 
@@ -1512,8 +1576,10 @@ You can use the {\discriminate} tactic.
 Inductive toto : Set := | C1 : toto | C2 : toto.
 Goal C1 <> C2.
 discriminate.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 \Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?}
 
@@ -1561,7 +1627,7 @@ If you type for instance the following ``definition'':
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Definition max (n p : nat) := if n <= p then p else n.
+Fail Definition max (n p : nat) := if n <= p then p else n.
 \end{coq_example}
 
 As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a
@@ -1729,7 +1795,7 @@ mergesort} as an example).
 the arguments of the loop.
 
 \begin{coq_eval}
-Open Scope R_scope.
+Reset Initial.
 Require Import List.
 \end{coq_eval}
 
@@ -1742,21 +1808,25 @@ Definition R (a b:list nat) := length a < length b.
 \begin{coq_example*}
 Lemma Rwf : well_founded R.
 \end{coq_example*}
+\begin{coq_eval}
+Admitted.
+\end{coq_eval}
 
 \item Define the step function (which needs proofs that recursive
 calls are on smaller arguments).
 
-\begin{verbatim}
-Definition split (l : list nat) 
-   : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}
-   := (* ... *) .
-Definition concat (l1 l2 : list nat) : list nat := (* ... *) .
+\begin{coq_example*}
+Definition split (l : list nat)
+   : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}.
+Admitted.
+Definition concat (l1 l2 : list nat) : list nat.
+Admitted.
 Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) :=
   let (lH1,lH2) := (split l) in
   let (l1,H1) := lH1 in
   let (l2,H2) := lH2 in
   concat (f l1 H1) (f l2 H2).
-\end{verbatim}
+\end{coq_example*}
 
 \item Define the recursive function by fixpoint on the step function.
 
@@ -1811,9 +1881,9 @@ induction 1.
   inversion 1.
   inversion 1. apply IHeven; trivial.
 \end{coq_example}
-\begin{coq_eval}
+\begin{coq_example*}
 Qed.
-\end{coq_eval}
+\end{coq_example*}
 
 In case the type of the second induction hypothesis is not
 dependent, {\tt inversion} can just be replaced by {\tt destruct}.
@@ -1848,10 +1918,10 @@ Double induction (or induction on pairs) is a restriction of the
 lexicographic induction. Here is an example of double induction.
 
 \begin{coq_example}
-Lemma nat_double_ind : 
-forall P : nat -> nat -> Prop, P 0 0 -> 
-  (forall m n, P m n -> P m (S n)) -> 
-  (forall m n, P m n -> P (S m) n) -> 
+Lemma nat_double_ind :
+forall P : nat -> nat -> Prop, P 0 0 ->
+  (forall m n, P m n -> P m (S n)) ->
+  (forall m n, P m n -> P (S m) n) ->
      forall m n, P m n.
 intros P H00 HmS HSn; induction m.
 (* case 0 *)
@@ -1859,9 +1929,9 @@ induction n; [assumption | apply HmS; apply IHn].
 (* case Sm *)
 intro n; apply HSn; apply IHm.
 \end{coq_example}
-\begin{coq_eval}
+\begin{coq_example*}
 Qed.
-\end{coq_eval}
+\end{coq_example*}
 
 \Question{How to define a function by nested recursion?}
 
@@ -1896,7 +1966,7 @@ Set Implicit Arguments.
 CoInductive Stream (A:Set) : Set :=
   Cons : A -> Stream A -> Stream A.
 CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)).
-Lemma Stream_unfold : 
+Lemma Stream_unfold :
    forall n:nat, nats n = Cons n (nats (S n)).
 Proof.
   intro;
@@ -1904,8 +1974,10 @@ Proof.
                   | Cons x s => Cons x s
                   end).
   case (nats n); reflexivity.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 
@@ -2586,8 +2658,10 @@ eapply eq_trans.
 Show Existentials.
 eassumption.
 assumption.
-Qed.
 \end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
 
 
 \Question{What can I do if I get ``Cannot solve a second-order unification problem''?}