diff options
author | 2004-05-06 17:13:30 +0000 | |
---|---|---|
committer | 2004-05-06 17:13:30 +0000 | |
commit | a81bc64b0d3e3e551ace7aea73f4b258d5724425 (patch) | |
tree | 7ba2004dff067b08edcae7f2063ad2da94b88218 | |
parent | c418cf663a26f8358c1e21fe4a37dc8c806b45cf (diff) |
Ajout �tudes de cas
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8573 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/newfaq/main.tex | 122 |
1 files changed, 104 insertions, 18 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index caad5de5a..553328eca 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -603,25 +603,21 @@ inconsistency} appears. Example: {\tt fun (x:Type) (y:$\forall$ X:Type, X \Question{I have two proofs of the same proposition. Can I prove they are equal?} -In the base {\Coq} system, the answer is no. However, if +In the base {\Coq} system, the answer is generally no. However, if classical logic is set, the answer is yes for propositions in {\Prop}. -See question \ref{proof-irrelevance}. +The answer is also yes if proof irrelevance holds (see question +\ref{proof-irrelevance}). + +There are also ``simple enough'' propositions for which you can prove +the equality without requiring any extra axioms. This is typically +the case for propositions defined deterministically as a first-order +inductive predicate on decidable sets. See for instance in question +\ref{le-uniqueness} an axiom-free proof of the unicity of the proofs of +the proposition {\tt le m n} (less or equal on {\tt nat}). % It is an ongoing work of research to natively include proof % irrelevance in {\Coq}. -\Question{Can I prove that the second components of equal dependent -pairs are equal?} - - The answer is the same as for proofs of equality -statements. It is provable if equality on the domain of the first -component is decidable (look at \verb=inj_right_pair= from file -\vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general -case. However, it is consistent (with the Calculus of Constructions) -to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually -provides an axiom (equivalent to Streicher's axiom $K$) which entails -the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}). - \Question{I have two proofs of an equality statement. Can I prove they are equal?} @@ -634,6 +630,18 @@ classical logic. All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}. +\Question{Can I prove that the second components of equal dependent +pairs are equal?} + + The answer is the same as for proofs of equality +statements. It is provable if equality on the domain of the first +component is decidable (look at \verb=inj_right_pair= from file +\vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general +case. However, it is consistent (with the Calculus of Constructions) +to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually +provides an axiom (equivalent to Streicher's axiom $K$) which entails +the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}). + \subsection{Impredicativity} \Question{Why {\tt injection} does not work on impredicative {\tt Set}?} @@ -1725,20 +1733,98 @@ Proof. Qed. \end{coq_example*} +\Question{Is there an axiom-free proof of Streicher's axiom $K$ for +the equality on {\tt nat}?} +\label{K-nat} + +Yes because equality is decidable on {\tt nat}. Here is the proof. + +\begin{coq_example*} +Require Import Eqdep_dec. +Require Import Peano_dec. +Theorem K_nat : + forall (x:nat) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. +Proof. +intros; apply K_dec_set with (p := p). +apply eq_nat_dec. +assumption. +Qed. +\end{coq_example*} + +Similarly, we have + +\begin{coq_example*} +Theorem eq_rect_eq_nat : + forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h. +Proof. +intros; apply K_nat with (p := h); reflexivity. +Qed. +\end{coq_example*} + +\Question{How to prove that two proofs of {\tt n<=m} on {\tt nat} are equal?} +\label{le-uniqueness} + +This is provable without requiring any axiom because axiom $K$ +directly holds on {\tt nat}. Here is a proof using question \ref{K-nat}. + +\begin{coq_example*} +Scheme le_ind' := Induction for le Sort Prop. +Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q. +Proof. +induction p using le_ind'; intro q. + replace (le_n n) with + (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)). + 2:reflexivity. + generalize (refl_equal n). + pattern n at 2 4 6 10, q; case q; [intro | intros m l e]. + rewrite <- eq_rect_eq_nat; trivial. + contradiction (le_Sn_n m); rewrite <- e; assumption. + replace (le_S n m p) with + (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))). + 2:reflexivity. + generalize (refl_equal (S m)). + pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS]. + contradiction (le_Sn_n m); rewrite Heq; assumption. + injection HeqS; intro Heq; generalize l HeqS. + rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat. + rewrite (IHp l0); reflexivity. +Qed. +\end{coq_example*} + \Question{How to exploit equalities on sets} - To extract information from an equality on sets, you need to +To extract information from an equality on sets, you need to find a predicate of sets satisfied by the elements of the sets. As an example, let's consider the following theorem. \begin{coq_example*} -Theorem le_le : +Theorem interval_discr : forall m n:nat, {x : nat | x <= m} = {x : nat | x <= n} -> m = n. \end{coq_example*} -A typical property is to have cardinality $n$. - +We have a proof requiring the axiom of proof-irrelevance. We +conjecture that proof-irrelevance can be circumvented by introducing a +primitive definition of discrimination of the proofs of +\verb!{x : nat | x <= m}!. + +\begin{latexonly}% +The proof can be found in file {\tt interval$\_$discr.v} in this directory. +%Here is the proof +%\begin{small} +%\begin{flushleft} +%\begin{texttt} +%\def_{\ifmmode\sb\else\subscr\fi} +%\include{interval_discr.v} +%%% WARNING semantics of \_ has changed ! +%\end{texttt} +%$a\_b\_c$ +%\end{flushleft} +%\end{small} +\end{latexonly}% +\begin{htmlonly}% +\ahref{./interval_discr.v}{Here} is the proof. +\end{htmlonly} \Question{I have a problem of dependent elimination on proofs, how to solve it?} |