diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b685e68e43..28fe68d78d 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -38,12 +38,12 @@ obligations which need to be resolved to create the final term. Elaborating programs --------------------- -The main difference from |Coq| is that an object in a type T : Set can -be considered as an object of type { x : T | P} for any wellformed P : -Prop. If we go from T to the subset of T verifying property P, we must -prove that the object under consideration verifies it. Russell will -generate an obligation for every such coercion. In the other -direction, Russell will automatically insert a projection. +The main difference from |Coq| is that an object in a type :g:`T : Set` can +be considered as an object of type :g:`{x : T | P}` for any well-formed +:g:`P : Prop`. If we go from :g:`T` to the subset of :g:`T` verifying property +:g:`P`, we must prove that the object under consideration verifies it. Russell +will generate an obligation for every such coercion. In the other direction, +Russell will automatically insert a projection. Another distinction is the treatment of pattern-matching. Apart from the following differences, it is equivalent to the standard match @@ -67,7 +67,7 @@ operation (see :ref:`extendedpatternmatching`). (match x as y return (x = y -> _) with | 0 => fun H : x = 0 -> t | S n => fun H : x = S n -> u - end) (eq_refl n). + end) (eq_refl x). This permits to get the proper equalities in the context of proof obligations inside clauses, without which reasoning is very limited. @@ -75,7 +75,7 @@ operation (see :ref:`extendedpatternmatching`). + Generation of inequalities. If a pattern intersects with a previous one, an inequality is added in the context of the second branch. See for example the definition of div2 below, where the second branch is - typed in a context where ∀ p, _ <> S (S p). + typed in a context where :g:`∀ p, _ <> S (S p)`. + Coercion. If the object being matched is coercible to an inductive type, the corresponding coercion will be automatically inserted. This also works with the previous mechanism. @@ -88,7 +88,7 @@ coercions. This controls the special treatment of pattern-matching generating equalities and inequalities when using |Program| (it is on by default). All - pattern-matchings and let-patterns are handled using the standard algorithm + pattern-matches and let-patterns are handled using the standard algorithm of |Coq| (see :ref:`extendedpatternmatching`) when this option is deactivated. @@ -108,9 +108,9 @@ typechecker will fall back directly to |Coq|’s usual typing of dependent pattern-matching if a return or in clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can -use the dec combinator to get the correct hypotheses as in: +use the :g:`dec` combinator to get the correct hypotheses as in: -.. coqtop:: none +.. coqtop:: in Require Import Program Arith. @@ -120,7 +120,7 @@ use the dec combinator to get the correct hypotheses as in: if dec (leb n 0) then 0 else S (pred n). -The let tupling construct :g:`let (x1, ..., xn) := t in b` does not +The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not produce an equality, contrary to the let pattern construct :g:`let ’(x1, ..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to coerce term to its support type. It can be useful in notations, for @@ -200,7 +200,7 @@ The structural fixpoint operator behaves just like the one of |Coq| (see :cmd:`Fixpoint`), except it may also generate obligations. It works with mutually recursive definitions too. -.. coqtop:: reset none +.. coqtop:: reset in Require Import Program Arith. @@ -264,7 +264,7 @@ Program Lemma Definition` and use it as the goal afterwards. Otherwise the proof will be started with the elaborated version as a goal. The :g:`Program` prefix can similarly be used as a prefix for - :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc... + :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc. .. _solving_obligations: @@ -300,7 +300,7 @@ optional tactic is replaced by the default one if not specified. Start the proof of the next unsolved obligation. -.. cmd:: Solve Obligations {? of @ident} {? with @tactic} +.. cmd:: Solve Obligations {? {? of @ident} with @tactic} Tries to solve each obligation of ``ident`` using the given ``tactic`` or the default one. @@ -322,13 +322,13 @@ optional tactic is replaced by the default one if not specified. .. opt:: Transparent Obligations - Control whether all obligations should be declared as transparent + Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. .. opt:: Hide Obligations - Control whether obligations appearing in the + Controls whether obligations appearing in the term should be hidden as implicit arguments of the special constantProgram.Tactics.obligation. |