diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b685e68e43..d6895f5fe5 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -18,7 +18,7 @@ program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the whole |Coq| proof apparatus. This is done using a technique originating from the “Predicate subtyping” mechanism of -PVS :cite:`Rushby98`, which generates type-checking conditions while typing a +PVS :cite:`Rushby98`, which generates type checking conditions while typing a term constrained to a particular type. Here we insert existential variables in the term, which must be filled with proofs to get a complete |Coq| term. |Program| replaces the |Program| tactic by Catherine @@ -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,15 +67,15 @@ 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. -+ Generation of inequalities. If a pattern intersects with a previous - one, an inequality is added in the context of the second branch. See ++ Generation of disequalities. If a pattern intersects with a previous + one, a disequality 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. @@ -87,8 +87,8 @@ coercions. .. opt:: Program Cases 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 + and disequalities when using |Program| (it is on by default). All + pattern-matches and let-patterns are handled using the standard algorithm of |Coq| (see :ref:`extendedpatternmatching`) when this option is deactivated. @@ -104,13 +104,13 @@ Syntactic control over equalities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To give more control over the generation of equalities, the -typechecker will fall back directly to |Coq|’s usual typing of dependent +type checker 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 @@ -175,7 +175,7 @@ Program Definition .. TODO refer to production in alias -See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` +.. seealso:: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` .. _program_fixpoint: @@ -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. |