diff options
Diffstat (limited to 'doc/faq')
| -rw-r--r-- | doc/faq/FAQ.tex | 242 | ||||
| -rw-r--r-- | doc/faq/axioms.eps | 417 | ||||
| -rw-r--r-- | doc/faq/axioms.eps_t | 43 | ||||
| -rw-r--r-- | doc/faq/axioms.pdf | bin | 4974 -> 0 bytes | |||
| -rw-r--r-- | doc/faq/axioms.pdf_t | 43 | ||||
| -rw-r--r-- | doc/faq/axioms.png | bin | 32222 -> 0 bytes |
6 files changed, 154 insertions, 591 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index b03aa64090..48b61827d1 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -228,7 +228,7 @@ kernel is intentionally small to limit the risk of conceptual or accidental implementation bugs. \item[The Objective Caml compiler] The {\Coq} kernel is written using the Objective Caml language but it uses only the most standard features -(no object, no label ...), so that it is highly unprobable that an +(no object, no label ...), so that it is highly improbable that an Objective Caml bug breaks the consistency of {\Coq} without breaking all other kinds of features of {\Coq} or of other software compiled with Objective Caml. @@ -509,22 +509,14 @@ library. (Statements in boldface are the most ``interesting'' ones for Coq.) The justification of their validity relies on the interpretability in set theory. -% fig2dev -m 2 -L png axioms.fig axioms.png -% fig2dev -L pdftex axioms.fig axioms.pdf -% fig2dev -L pdftex_t -p axioms.pdf axioms.fig axioms.pdf_t -% fig2dev -L pstex axioms.fig axioms.eps -% fig2dev -L pstex_t -p axioms.eps axioms.fig axioms.eps_t - \begin{figure}[htbp] %HEVEA\imgsrc{axioms.png} %BEGIN LATEX \begin{center} \ifpdf % si on est en pdflatex \scalebox{0.65}{\input{axioms.pdf_t}} -%\includegraphics[width=1.0\textwidth]{axioms.png} \else \scalebox{0.65}{\input{axioms.eps_t}} -%\includegraphics[width=1.0\textwidth]{axioms.eps} \fi \end{center} %END LATEX @@ -718,7 +710,7 @@ 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 +\ref{le-uniqueness} an axiom-free proof of the uniqueness 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 @@ -849,26 +841,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 +885,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 +914,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 +946,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 +967,10 @@ Qed. Goal 3+0 = 3. apply mylemma. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} @@ -972,8 +987,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 +1004,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. +As with conjunctive hypotheses, you can use the {\destruct} tactic or +the {\intros} tactic to decompose them into several hypotheses. -\Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different 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 +1029,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 +1043,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 +1058,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 +1097,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 +1133,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 +1146,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 +1165,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 +1185,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 +1199,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 +1213,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 +1229,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 +1275,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 +1381,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 +1397,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 +1412,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 +1427,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?} @@ -1441,7 +1497,7 @@ while {\assert} is. \Question{What can I do if \Coq can not infer some implicit argument ?} -You can state explicitely what this implicit argument is. See \ref{implicit}. +You can state explicitly what this implicit argument is. See \ref{implicit}. \Question{How can I explicit some implicit argument ?}\label{implicit} @@ -1512,8 +1568,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,20 +1619,20 @@ 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 statement that belongs to the mathematical world. There are many ways to prove such a proposition, either by some computation, or using some already -proven theoremas. For instance, proving $3-2 \leq 2^{45503}$ is very easy, +proven theorems. For instance, proving $3-2 \leq 2^{45503}$ is very easy, using some theorems on arithmetical operations. If you compute both numbers before comparing them, you risk to use a lot of time and space. On the contrary, a function for computing the greatest of two natural numbers is an algorithm which, called on two natural numbers -$n$ and $p$, determines wether $n\leq p$ or $p < n$. +$n$ and $p$, determines whether $n\leq p$ or $p < n$. Such a function is a \emph{decision procedure} for the inequality of \texttt{nat}. The possibility of writing such a procedure comes directly from de decidability of the order $\leq$ on natural numbers. @@ -1648,7 +1706,7 @@ immediate, whereas one can't wait for the result of This is normal. Your definition is a simple recursive function which returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified -function}, i.e. a complex object, able not only to tell wether $n\leq p$ +function}, i.e. a complex object, able not only to tell whether $n\leq p$ or $p<n$, but also of building a complete proof of the correct inequality. What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min} and \texttt{max} is the building of a huge proof term. @@ -1729,7 +1787,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 +1800,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 +1873,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 +1910,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 +1921,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 +1958,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 +1966,10 @@ Proof. | Cons x s => Cons x s end). case (nats n); reflexivity. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} @@ -2340,8 +2404,8 @@ You can use {\tt coqdoc}. \Question{How can I generate some dependency graph from my development?} -You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002. -This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/). +You can use the tool \verb|coqgraph| developed by Philippe Audebaud in 2002. +This tool transforms dependencies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/). \Question{How can I cite some {\Coq} in my latex document?} @@ -2475,7 +2539,7 @@ modifiers keys available through GTK. The straightest way to get rid of the problem is to edit by hand your coqiderc (either \verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\ \verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) - and replace any occurence of \texttt{MOD4} by \texttt{MOD1}. +and replace any occurrence of \texttt{MOD4} by \texttt{MOD1}. @@ -2574,7 +2638,7 @@ existential variable which eventually got erased by some computation. You may backtrack to the faulty occurrence of {\eauto} or {\eapply} and give the missing argument an explicit value. Alternatively, you can use the commands \texttt{Show Existentials.} and -\texttt{Existential.} to display and instantiate the remainig +\texttt{Existential.} to display and instantiate the remaining existential variables. @@ -2586,8 +2650,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''?} diff --git a/doc/faq/axioms.eps b/doc/faq/axioms.eps deleted file mode 100644 index 836afc3474..0000000000 --- a/doc/faq/axioms.eps +++ /dev/null @@ -1,417 +0,0 @@ -%!PS-Adobe-3.0 EPSF-3.0 -%%Title: axioms.fig -%%Creator: fig2dev Version 3.2 Patchlevel 5e -%%CreationDate: Sun Jul 26 08:23:54 2015 -%%BoundingBox: 0 0 647 514 -%Magnification: 1.0000 -%%EndComments -%%BeginProlog -/$F2psDict 200 dict def -$F2psDict begin -$F2psDict /mtrx matrix put -/col-1 {0 setgray} bind def -/col0 {0.000 0.000 0.000 srgb} bind def -/col1 {0.000 0.000 1.000 srgb} bind def -/col2 {0.000 1.000 0.000 srgb} bind def -/col3 {0.000 1.000 1.000 srgb} bind def -/col4 {1.000 0.000 0.000 srgb} bind def -/col5 {1.000 0.000 1.000 srgb} bind def -/col6 {1.000 1.000 0.000 srgb} bind def -/col7 {1.000 1.000 1.000 srgb} bind def -/col8 {0.000 0.000 0.560 srgb} bind def -/col9 {0.000 0.000 0.690 srgb} bind def -/col10 {0.000 0.000 0.820 srgb} bind def -/col11 {0.530 0.810 1.000 srgb} bind def -/col12 {0.000 0.560 0.000 srgb} bind def -/col13 {0.000 0.690 0.000 srgb} bind def -/col14 {0.000 0.820 0.000 srgb} bind def -/col15 {0.000 0.560 0.560 srgb} bind def -/col16 {0.000 0.690 0.690 srgb} bind def -/col17 {0.000 0.820 0.820 srgb} bind def -/col18 {0.560 0.000 0.000 srgb} bind def -/col19 {0.690 0.000 0.000 srgb} bind def -/col20 {0.820 0.000 0.000 srgb} bind def -/col21 {0.560 0.000 0.560 srgb} bind def -/col22 {0.690 0.000 0.690 srgb} bind def -/col23 {0.820 0.000 0.820 srgb} bind def -/col24 {0.500 0.190 0.000 srgb} bind def -/col25 {0.630 0.250 0.000 srgb} bind def -/col26 {0.750 0.380 0.000 srgb} bind def -/col27 {1.000 0.500 0.500 srgb} bind def -/col28 {1.000 0.630 0.630 srgb} bind def -/col29 {1.000 0.750 0.750 srgb} bind def -/col30 {1.000 0.880 0.880 srgb} bind def -/col31 {1.000 0.840 0.000 srgb} bind def - -end - -/cp {closepath} bind def -/ef {eofill} bind def -/gr {grestore} bind def -/gs {gsave} bind def -/sa {save} bind def -/rs {restore} bind def -/l {lineto} bind def -/m {moveto} bind def -/rm {rmoveto} bind def -/n {newpath} bind def -/s {stroke} bind def -/sh {show} bind def -/slc {setlinecap} bind def -/slj {setlinejoin} bind def -/slw {setlinewidth} bind def -/srgb {setrgbcolor} bind def -/rot {rotate} bind def -/sc {scale} bind def -/sd {setdash} bind def -/ff {findfont} bind def -/sf {setfont} bind def -/scf {scalefont} bind def -/sw {stringwidth} bind def -/tr {translate} bind def -/tnt {dup dup currentrgbcolor - 4 -2 roll dup 1 exch sub 3 -1 roll mul add - 4 -2 roll dup 1 exch sub 3 -1 roll mul add - 4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb} - bind def -/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul - 4 -2 roll mul srgb} bind def -/$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def -/$F2psEnd {$F2psEnteredState restore end} def - -/pageheader { -save -newpath 0 514 moveto 0 0 lineto 647 0 lineto 647 514 lineto closepath clip newpath --26.1 566.6 translate -1 -1 scale -$F2psBegin -10 setmiterlimit -0 slj 0 slc - 0.06000 0.06000 sc -} bind def -/pagefooter { -$F2psEnd -restore -} bind def -%%EndProlog -pageheader -% -% Fig objects follow -% -% -% here starts figure with depth 50 -% Arc -7.500 slw -0 slc -gs clippath -4188 5861 m 4168 6010 l 4227 6018 l 4247 5869 l 4247 5869 l 4202 5984 l 4188 5861 l cp -eoclip -n 14032.5 7222.5 9908.2 -159.9465 -172.9126 arcn -gs col0 s gr - gr - -% arrowhead -0 slj -n 4188 5861 m 4202 5984 l 4247 5869 l 4188 5861 l cp gs 0.00 setgray ef gr col0 s -% Arc -gs clippath -3465 9040 m 3599 9108 l 3626 9054 l 3492 8987 l 3492 8987 l 3586 9068 l 3465 9040 l cp -eoclip -n 3600.0 8925.0 150.0 90.0000 -90.0000 arc -gs col0 s gr - gr - -% arrowhead -n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 l cp gs 0.00 setgray ef gr col0 s -% Arc -gs clippath -3465 8740 m 3599 8808 l 3626 8754 l 3492 8687 l 3492 8687 l 3586 8768 l 3465 8740 l cp -eoclip -n 3600.0 8625.0 150.0 90.0000 -90.0000 arc -gs col0 s gr - gr - -% arrowhead -n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 l cp gs 0.00 setgray ef gr col0 s -% Arc -gs clippath -3492 8262 m 3626 8195 l 3599 8141 l 3465 8209 l 3465 8209 l 3586 8182 l 3492 8262 l cp -3465 8440 m 3599 8508 l 3626 8454 l 3492 8387 l 3492 8387 l 3586 8468 l 3465 8440 l cp -eoclip -n 3600.0 8325.0 150.0 90.0000 -90.0000 arc -gs col0 s gr - gr - -% arrowhead -n 3465 8440 m 3586 8468 l 3492 8387 l 3465 8440 l cp gs 0.00 setgray ef gr col0 s -% arrowhead -n 3492 8262 m 3586 8182 l 3465 8209 l 3492 8262 l cp gs 0.00 setgray ef gr col0 s -% Arc -gs clippath -3492 8562 m 3626 8495 l 3599 8441 l 3465 8509 l 3465 8509 l 3586 8482 l 3492 8562 l cp -3465 8740 m 3599 8808 l 3626 8754 l 3492 8687 l 3492 8687 l 3586 8768 l 3465 8740 l cp -eoclip -n 3600.0 8625.0 150.0 90.0000 -90.0000 arc -gs col0 s gr - gr - -% arrowhead -n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 l cp gs 0.00 setgray ef gr col0 s -% arrowhead -n 3492 8562 m 3586 8482 l 3465 8509 l 3492 8562 l cp gs 0.00 setgray ef gr col0 s -% Arc -gs clippath -3492 8862 m 3626 8795 l 3599 8741 l 3465 8809 l 3465 8809 l 3586 8782 l 3492 8862 l cp -3465 9040 m 3599 9108 l 3626 9054 l 3492 8987 l 3492 8987 l 3586 9068 l 3465 9040 l cp -eoclip -n 3600.0 8925.0 150.0 90.0000 -90.0000 arc -gs col0 s gr - gr - -% arrowhead -n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 l cp gs 0.00 setgray ef gr col0 s -% arrowhead -n 3492 8862 m 3586 8782 l 3465 8809 l 3492 8862 l cp gs 0.00 setgray ef gr col0 s -% Arc -gs clippath -3492 9162 m 3626 9095 l 3599 9041 l 3465 9109 l 3465 9109 l 3586 9082 l 3492 9162 l cp -3465 9340 m 3599 9408 l 3626 9354 l 3492 9287 l 3492 9287 l 3586 9368 l 3465 9340 l cp -eoclip -n 3600.0 9225.0 150.0 90.0000 -90.0000 arc -gs col0 s gr - gr - -% arrowhead -n 3465 9340 m 3586 9368 l 3492 9287 l 3465 9340 l cp gs 0.00 setgray ef gr col0 s -% arrowhead -n 3492 9162 m 3586 9082 l 3465 9109 l 3492 9162 l cp gs 0.00 setgray ef gr col0 s -% Arc -gs clippath -3733 7095 m 3805 7227 l 3858 7198 l 3785 7066 l 3785 7066 l 3817 7186 l 3733 7095 l cp -eoclip -n 6309.5 5767.7 2867.8 -137.3570 150.0374 arcn -gs col0 s gr - gr - -% arrowhead -n 3733 7095 m 3817 7186 l 3785 7066 l 3733 7095 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -7204 5860 m 7167 6007 l 7225 6021 l 7262 5874 l 7262 5874 l 7204 5984 l 7204 5860 l cp -eoclip -n 7725 3900 m - 7200 6000 l gs col0 s gr gr - -% arrowhead -n 7204 5860 m 7204 5984 l 7262 5874 l 7204 5860 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -7170 6914 m 7170 7065 l 7230 7065 l 7230 6914 l 7230 6914 l 7200 7034 l 7170 6914 l cp -eoclip -n 7200 6225 m - 7200 7050 l gs col0 s gr gr - -% arrowhead -n 7170 6914 m 7200 7034 l 7230 6914 l 7170 6914 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -5520 5864 m 5520 6015 l 5580 6015 l 5580 5864 l 5580 5864 l 5550 5984 l 5520 5864 l cp -5580 5761 m 5580 5610 l 5520 5610 l 5520 5761 l 5520 5761 l 5550 5641 l 5580 5761 l cp -eoclip -n 5550 5625 m - 5550 6000 l gs col0 s gr gr - -% arrowhead -n 5580 5761 m 5550 5641 l 5520 5761 l 5580 5761 l cp gs 0.00 setgray ef gr col0 s -% arrowhead -n 5520 5864 m 5550 5984 l 5580 5864 l 5520 5864 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -3345 3464 m 3345 3615 l 3405 3615 l 3405 3464 l 3405 3464 l 3375 3584 l 3345 3464 l cp -3405 3361 m 3405 3210 l 3345 3210 l 3345 3361 l 3345 3361 l 3375 3241 l 3405 3361 l cp -eoclip -n 3375 3225 m - 3375 3600 l gs col0 s gr gr - -% arrowhead -n 3405 3361 m 3375 3241 l 3345 3361 l 3405 3361 l cp gs 0.00 setgray ef gr col0 s -% arrowhead -n 3345 3464 m 3375 3584 l 3405 3464 l 3345 3464 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -3344 2114 m 3346 2265 l 3406 2264 l 3404 2113 l 3404 2113 l 3376 2234 l 3344 2114 l cp -eoclip -n 3373 1950 m - 3376 2250 l gs col0 s gr gr - -% arrowhead -n 3344 2114 m 3376 2234 l 3404 2113 l 3344 2114 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -3345 2864 m 3345 3015 l 3405 3015 l 3405 2864 l 3405 2864 l 3375 2984 l 3345 2864 l cp -3405 2761 m 3405 2610 l 3345 2610 l 3345 2761 l 3345 2761 l 3375 2641 l 3405 2761 l cp -eoclip -n 3375 2625 m - 3375 3000 l gs col0 s gr gr - -% arrowhead -n 3405 2761 m 3375 2641 l 3345 2761 l 3405 2761 l cp gs 0.00 setgray ef gr col0 s -% arrowhead -n 3345 2864 m 3375 2984 l 3405 2864 l 3345 2864 l cp gs 0.00 setgray ef gr col0 s -% Polyline -n 2175 3600 m - 3750 3600 l gs col0 s gr -% Polyline -gs clippath -2611 2445 m 2460 2445 l 2460 2505 l 2611 2505 l 2611 2505 l 2491 2475 l 2611 2445 l cp -eoclip -n 3075 2475 m - 2475 2475 l gs col0 s gr gr - -% arrowhead -n 2611 2445 m 2491 2475 l 2611 2505 l 2611 2445 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -3345 1289 m 3347 1440 l 3407 1439 l 3405 1288 l 3405 1288 l 3377 1409 l 3345 1289 l cp -eoclip -n 3374 1125 m - 3377 1425 l gs col0 s gr gr - -% arrowhead -n 3345 1289 m 3377 1409 l 3405 1288 l 3345 1289 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -1711 945 m 1560 945 l 1560 1005 l 1711 1005 l 1711 1005 l 1591 975 l 1711 945 l cp -eoclip -n 3075 975 m - 1575 975 l gs col0 s gr gr - -% arrowhead -n 1711 945 m 1591 975 l 1711 1005 l 1711 945 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -2161 1695 m 2010 1695 l 2010 1755 l 2161 1755 l 2161 1755 l 2041 1725 l 2161 1695 l cp -eoclip -n 3075 1725 m - 2025 1725 l gs col0 s gr gr - -% arrowhead -n 2161 1695 m 2041 1725 l 2161 1755 l 2161 1695 l cp gs 0.00 setgray ef gr col0 s -% Polyline -n 8025 5925 m 8250 5925 l 9000 4950 l - 9150 4950 l gs col0 s gr -% Polyline -gs clippath -8312 4025 m 8275 3878 l 8217 3892 l 8254 4039 l 8254 4039 l 8254 3916 l 8312 4025 l cp -eoclip -n 8625 5400 m - 8250 3900 l gs col0 s gr gr - -% arrowhead -n 8312 4025 m 8254 3916 l 8254 4039 l 8312 4025 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -4700 7888 m 4553 7924 l 4567 7982 l 4714 7946 l 4714 7946 l 4591 7946 l 4700 7888 l cp -eoclip -n 7050 7350 m - 4575 7950 l gs col0 s gr gr - -% arrowhead -n 4700 7888 m 4591 7946 l 4714 7946 l 4700 7888 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -4170 7814 m 4170 7965 l 4230 7965 l 4230 7814 l 4230 7814 l 4200 7934 l 4170 7814 l cp -eoclip -n 4200 7500 m - 4200 7950 l gs col0 s gr gr - -% arrowhead -n 4170 7814 m 4200 7934 l 4230 7814 l 4170 7814 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -1295 3398 m 1339 3543 l 1397 3526 l 1353 3381 l 1353 3381 l 1359 3505 l 1295 3398 l cp -1207 2893 m 1163 2748 l 1105 2765 l 1149 2910 l 1149 2910 l 1144 2787 l 1207 2893 l cp -eoclip -n 1139 2771 m - 1364 3521 l gs col0 s gr gr - -% arrowhead -n 1207 2893 m 1144 2787 l 1149 2910 l 1207 2893 l cp gs 0.00 setgray ef gr col0 s -% arrowhead -n 1295 3398 m 1359 3505 l 1353 3381 l 1295 3398 l cp gs 0.00 setgray ef gr col0 s -% Polyline -n 4425 4875 m - 7350 3825 l gs col0 s gr -% Polyline -gs clippath -1019 1289 m 1021 1440 l 1081 1439 l 1079 1288 l 1079 1288 l 1051 1409 l 1019 1289 l cp -eoclip -n 1048 1125 m - 1051 1425 l gs col0 s gr gr - -% arrowhead -n 1019 1289 m 1051 1409 l 1079 1288 l 1019 1289 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -1020 2114 m 1022 2265 l 1082 2264 l 1080 2113 l 1080 2113 l 1052 2234 l 1020 2114 l cp -eoclip -n 1049 1950 m - 1052 2250 l gs col0 s gr gr - -% arrowhead -n 1020 2114 m 1052 2234 l 1080 2113 l 1020 2114 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -2104 5879 m 2151 6023 l 2208 6005 l 2161 5861 l 2161 5861 l 2170 5985 l 2104 5879 l cp -eoclip -n 1500 3900 m - 2175 6000 l gs col0 s gr gr - -% arrowhead -n 2104 5879 m 2170 5985 l 2161 5861 l 2104 5879 l cp gs 0.00 setgray ef gr col0 s -% Polyline -n 4575 6000 m - 6450 6000 l gs col0 s gr -% Polyline -gs clippath -6900 7063 m 7043 7113 l 7063 7056 l 6920 7006 l 6920 7006 l 7024 7075 l 6900 7063 l cp -eoclip -n 4714 6255 m - 7039 7080 l gs col0 s gr gr - -% arrowhead -n 6900 7063 m 7024 7075 l 6920 7006 l 6900 7063 l cp gs 0.00 setgray ef gr col0 s -% Polyline -gs clippath -4170 7064 m 4170 7215 l 4230 7215 l 4230 7064 l 4230 7064 l 4200 7184 l 4170 7064 l cp -eoclip -n 4200 6225 m - 4200 7200 l gs col-1 s gr gr - -% arrowhead -n 4170 7064 m 4200 7184 l 4230 7064 l 4170 7064 l cp gs 0.00 setgray ef gr col-1 s -% Polyline -2 slj -n 6450 7050 m 6448 7050 l 6444 7049 l 6437 7048 l 6425 7046 l 6408 7044 l - 6385 7040 l 6356 7036 l 6320 7030 l 6279 7024 l 6231 7017 l - 6177 7008 l 6118 6999 l 6054 6990 l 5986 6979 l 5915 6969 l - 5841 6958 l 5766 6946 l 5690 6935 l 5614 6924 l 5539 6913 l - 5464 6902 l 5391 6891 l 5320 6881 l 5252 6871 l 5185 6861 l - 5122 6852 l 5061 6843 l 5002 6835 l 4947 6827 l 4894 6820 l - 4843 6813 l 4796 6807 l 4750 6801 l 4707 6796 l 4666 6791 l - 4627 6786 l 4590 6782 l 4555 6778 l 4521 6774 l 4489 6771 l - 4458 6768 l 4429 6765 l 4400 6763 l 4350 6759 l 4303 6755 l - 4258 6753 l 4216 6751 l 4176 6751 l 4138 6750 l 4102 6751 l - 4068 6752 l 4037 6754 l 4008 6757 l 3980 6760 l 3955 6764 l - 3933 6768 l 3912 6773 l 3894 6778 l 3877 6784 l 3863 6790 l - 3850 6796 l 3839 6803 l 3829 6810 l 3820 6816 l 3813 6823 l - 3806 6830 l 3800 6838 l 3791 6850 l 3783 6863 l 3776 6878 l - 3771 6894 l 3766 6912 l 3762 6932 l 3759 6954 l 3756 6977 l - 3753 7000 l 3752 7021 l 3751 7036 l 3750 7045 l 3750 7049 l - - 3750 7050 l gs col0 s gr -% here ends figure; -pagefooter -showpage -%%Trailer -%EOF diff --git a/doc/faq/axioms.eps_t b/doc/faq/axioms.eps_t deleted file mode 100644 index 38f1a3fed4..0000000000 --- a/doc/faq/axioms.eps_t +++ /dev/null @@ -1,43 +0,0 @@ -\begin{picture}(0,0)% -\includegraphics{axioms.eps}% -\end{picture}% -\setlength{\unitlength}{3947sp}% -% -\begingroup\makeatletter\ifx\SetFigFont\undefined% -\gdef\SetFigFont#1#2#3#4#5{% - \reset@font\fontsize{#1}{#2pt}% - \fontfamily{#3}\fontseries{#4}\fontshape{#5}% - \selectfont}% -\fi\endgroup% -\begin{picture}(10779,8553)(436,-8605) -\put(3676,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Excluded-middle}}}} -\put(451,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Operator iota}}}} -\put(3151,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive indefinite description}}}} -\put(3151,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}} -\put(451,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive definite descr.}}}} -\put(451,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}} -\put(3826,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Relational choice axiom}}}} -\put(6901,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Predicate extensionality}}}} -\put(1276,-4186){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(if Set impredicative)}}}} -\put(3751,-4411){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Diaconescu)}}}} -\put(4951,-4711){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional degeneracy}}}} -\put(6151,-5311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional extensionality}}}} -\put(4951,-5686){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(needs Prop-impredicativity)}}}} -\put(6001,-5911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Berardi)}}}} -\put(1576,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Not excluded-middle}}}} -\put(3376,-6586){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Decidability of equality on any A}}}} -\put(3601,-7336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Axiom K on A}}}} -\put(3601,-7636){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of reflexivity proofs for equality on A}}}} -\put(3601,-7936){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of equality proofs on A}}}} -\put(3601,-8536){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Invariance by substitution of reflexivity proofs for equality on A}}}} -\put(9001,-4336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional extensionality}}}} -\put(3601,-8236){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Injectivity of equality on Sigma-types on A}}}} -\put(6451,-6436){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Proof-irrelevance}}}} -\put(3151,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Operator epsilon}}}} -\put(3151,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}} -\put(3151,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}indefinite description}}}} -\put(3151,-2311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional choice axiom}}}} -\put(451,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}} -\put(451,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}definite description}}}} -\put(451,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Axiom of unique choice}}}} -\end{picture}% diff --git a/doc/faq/axioms.pdf b/doc/faq/axioms.pdf Binary files differdeleted file mode 100644 index 2ba5bf85b6..0000000000 --- a/doc/faq/axioms.pdf +++ /dev/null diff --git a/doc/faq/axioms.pdf_t b/doc/faq/axioms.pdf_t deleted file mode 100644 index 06dc4b280d..0000000000 --- a/doc/faq/axioms.pdf_t +++ /dev/null @@ -1,43 +0,0 @@ -\begin{picture}(0,0)% -\includegraphics{axioms.pdf}% -\end{picture}% -\setlength{\unitlength}{3947sp}% -% -\begingroup\makeatletter\ifx\SetFigFont\undefined% -\gdef\SetFigFont#1#2#3#4#5{% - \reset@font\fontsize{#1}{#2pt}% - \fontfamily{#3}\fontseries{#4}\fontshape{#5}% - \selectfont}% -\fi\endgroup% -\begin{picture}(10779,8553)(436,-8605) -\put(3676,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Excluded-middle}}}} -\put(451,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Operator iota}}}} -\put(3151,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive indefinite description}}}} -\put(3151,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}} -\put(451,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive definite descr.}}}} -\put(451,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}} -\put(3826,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Relational choice axiom}}}} -\put(6901,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Predicate extensionality}}}} -\put(1276,-4186){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(if Set impredicative)}}}} -\put(3751,-4411){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Diaconescu)}}}} -\put(4951,-4711){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional degeneracy}}}} -\put(6151,-5311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional extensionality}}}} -\put(4951,-5686){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(needs Prop-impredicativity)}}}} -\put(6001,-5911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Berardi)}}}} -\put(1576,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Not excluded-middle}}}} -\put(3376,-6586){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Decidability of equality on any A}}}} -\put(3601,-7336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Axiom K on A}}}} -\put(3601,-7636){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of reflexivity proofs for equality on A}}}} -\put(3601,-7936){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of equality proofs on A}}}} -\put(3601,-8536){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Invariance by substitution of reflexivity proofs for equality on A}}}} -\put(9001,-4336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional extensionality}}}} -\put(3601,-8236){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Injectivity of equality on Sigma-types on A}}}} -\put(6451,-6436){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Proof-irrelevance}}}} -\put(3151,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Operator epsilon}}}} -\put(3151,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}} -\put(3151,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}indefinite description}}}} -\put(3151,-2311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional choice axiom}}}} -\put(451,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}} -\put(451,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}definite description}}}} -\put(451,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Axiom of unique choice}}}} -\end{picture}% diff --git a/doc/faq/axioms.png b/doc/faq/axioms.png Binary files differdeleted file mode 100644 index a86eed7f12..0000000000 --- a/doc/faq/axioms.png +++ /dev/null |
