diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Basics.v | 18 | ||||
| -rw-r--r-- | theories/Program/Combinators.v | 16 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 325 | ||||
| -rw-r--r-- | theories/Program/FunctionalExtensionality.v | 109 | ||||
| -rw-r--r-- | theories/Program/Program.v | 9 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 5 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 24 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 52 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 4 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 207 |
10 files changed, 601 insertions, 168 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index a1a78acc..29494069 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -5,19 +5,19 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id: Basics.v 11709 2008-12-20 11:42:15Z msozeau $ *) -(* Standard functions and combinators. - * Proofs about them require functional extensionality and can be found in [Combinators]. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** Standard functions and combinators. + + Proofs about them require functional extensionality and can be found in [Combinators]. -(* $Id: Basics.v 11046 2008-06-03 22:48:06Z msozeau $ *) + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - Université Paris Sud + 91405 Orsay, France *) -(** The polymorphic identity function. *) +(** The polymorphic identity function is defined in [Datatypes]. *) -Definition id {A} := fun x : A => x. +Implicit Arguments id [[A]]. (** Function composition. *) diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index e267fbbe..ae9749de 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -5,15 +5,16 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id: Combinators.v 11709 2008-12-20 11:42:15Z msozeau $ *) -(* Proofs about standard combinators, exports functional extensionality. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** Proofs about standard combinators, exports functional extensionality. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) Require Import Coq.Program.Basics. -Require Export Coq.Program.FunctionalExtensionality. +Require Export FunctionalExtensionality. Open Scope program_scope. @@ -40,7 +41,8 @@ Proof. reflexivity. Qed. -Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core. +Hint Rewrite @compose_id_left @compose_id_right : core. +Hint Rewrite <- @compose_assoc : core. (** [flip] is involutive. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index c776070a..99d54755 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs-U") -*- *) +(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: Equality.v 11709 2008-12-20 11:42:15Z msozeau $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -20,6 +20,10 @@ Require Import Coq.Program.Tactics. Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level). +(** Notation for the single element of [x = x] *) + +Notation "'refl'" := (@refl_equal _ _). + (** Do something on an heterogeneous equality appearing in the context. *) Ltac on_JMeq tac := @@ -30,7 +34,7 @@ Ltac on_JMeq tac := (** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) Ltac simpl_one_JMeq := - on_JMeq ltac:(fun H => replace_hyp H (JMeq_eq H)). + on_JMeq ltac:(fun H => apply JMeq_eq in H). (** Repeat it for every possible hypothesis. *) @@ -185,7 +189,6 @@ Ltac simplify_eqs := (** A tactic that tries to remove trivial equality guards in induction hypotheses coming from [dependent induction]/[generalize_eqs] invocations. *) - Ltac simpl_IH_eq H := match type of H with | @JMeq _ ?x _ _ -> _ => @@ -224,9 +227,291 @@ Ltac do_simpl_IHs_eqs := Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs. -Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; +(** We split substitution tactics in the two directions depending on which + names we want to keep corresponding to the generalization performed by the + [generalize_eqs] tactic. *) + +Ltac subst_left_no_fail := + repeat (match goal with + [ H : ?X = ?Y |- _ ] => subst X + end). + +Ltac subst_right_no_fail := + repeat (match goal with + [ H : ?X = ?Y |- _ ] => subst Y + end). + +Ltac inject_left H := + progress (inversion H ; subst_left_no_fail ; clear_dups) ; clear H. + +Ltac inject_right H := + progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H. + +Ltac autoinjections_left := repeat autoinjection ltac:inject_left. +Ltac autoinjections_right := repeat autoinjection ltac:inject_right. + +Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; + simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs. + +Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ; simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs. +Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ; + simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs. + +(** Support for the [Equations] command. + These tactics implement the necessary machinery to solve goals produced by the + [Equations] command relative to dependent pattern-matching. + It is completely inspired from the "Eliminating Dependent Pattern-Matching" paper by + Goguen, McBride and McKinna. *) + + +(** The NoConfusionPackage class provides a method for making progress on proving a property + [P] implied by an equality on an inductive type [I]. The type of [noConfusion] for a given + [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where + [NoConfusion P x y] for constructor-headed [x] and [y] will give a formula ending in [P]. + This gives a general method for simplifying by discrimination or injectivity of constructors. + + Some actual instances are defined later in the file using the more primitive [discriminate] and + [injection] tactics on which we can always fall back. + *) + +Class NoConfusionPackage (I : Type) := { NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P }. + +(** The [DependentEliminationPackage] provides the default dependent elimination principle to + be used by the [equations] resolver. It is especially useful to register the dependent elimination + principles for things in [Prop] which are not automatically generated. *) + +Class DependentEliminationPackage (A : Type) := + { elim_type : Type ; elim : elim_type }. + +(** A higher-order tactic to apply a registered eliminator. *) + +Ltac elim_tac tac p := + let ty := type of p in + let eliminator := eval simpl in (elim (A:=ty)) in + tac p eliminator. + +(** Specialization to do case analysis or induction. + Note: the [equations] tactic tries [case] before [elim_case]: there is no need to register + generated induction principles. *) + +Ltac elim_case p := elim_tac ltac:(fun p el => destruct p using el) p. +Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p. + +(** The [BelowPackage] class provides the definition of a [Below] predicate for some datatype, + allowing to talk about course-of-value recursion on it. *) + +Class BelowPackage (A : Type) := { + Below : A -> Type ; + below : Π (a : A), Below a }. + +(** The [Recursor] class defines a recursor on a type, based on some definition of [Below]. *) + +Class Recursor (A : Type) (BP : BelowPackage A) := + { rec_type : A -> Type ; rec : Π (a : A), rec_type a }. + +(** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *) + +Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x). +Proof. intros; subst. apply X. Defined. + +Lemma solution_right : Π A (B : A -> Type) (t : A), B t -> (Π x, t = x -> B x). +Proof. intros; subst; apply X. Defined. + +Lemma deletion : Π A B (t : A), B -> (t = t -> B). +Proof. intros; assumption. Defined. + +Lemma simplification_heq : Π A B (x y : A), (x = y -> B) -> (JMeq x y -> B). +Proof. intros; apply X; apply (JMeq_eq H). Defined. + +Lemma simplification_existT2 : Π A (P : A -> Type) B (p : A) (x y : P p), + (x = y -> B) -> (existT P p x = existT P p y -> B). +Proof. intros. apply X. apply inj_pair2. exact H. Defined. + +Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P q), + (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B). +Proof. intros. injection H. intros ; auto. Defined. + +Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p). +Proof. intros. rewrite (UIP_refl A). assumption. Defined. + +(** This hint database and the following tactic can be used with [autosimpl] to + unfold everything to [eq_rect]s. *) + +Hint Unfold solution_left solution_right deletion simplification_heq + simplification_existT1 simplification_existT2 + eq_rect_r eq_rec eq_ind : equations. + +(** Simply unfold as much as possible. *) + +Ltac unfold_equations := repeat progress autosimpl with equations. + +(** The tactic [simplify_equations] is to be used when a program generated using [Equations] + is in the goal. It simplifies it as much as possible, possibly using [K] if needed. *) + +Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs). + +(** We will use the [block_induction] definition to separate the goal from the + equalities generated by the tactic. *) + +Definition block_dep_elim {A : Type} (a : A) := a. + +(** Using these we can make a simplifier that will perform the unification + steps needed to put the goal in normalised form (provided there are only + constructor forms). Compare with the lemma 16 of the paper. + We don't have a [noCycle] procedure yet. *) + +Ltac simplify_one_dep_elim_term c := + match c with + | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _) + | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _) + | eq (existT _ _ _) (existT _ _ _) -> _ => + refine (simplification_existT2 _ _ _ _ _ _ _) || + refine (simplification_existT1 _ _ _ _ _ _ _ _) + | ?x = ?y -> _ => (* variables case *) + (let hyp := fresh in intros hyp ; + move hyp before x ; + generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) || + (let hyp := fresh in intros hyp ; + move hyp before y ; + generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0) + | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P) + | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H) + | ?t = ?u -> _ => let hyp := fresh in + intros hyp ; elimtype False ; discriminate + | ?x = ?y -> _ => let hyp := fresh in + intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ; + case hyp ; clear hyp + | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *) + | _ => intro + end. + +Ltac simplify_one_dep_elim := + match goal with + | [ |- ?gl ] => simplify_one_dep_elim_term gl + end. + +(** Repeat until no progress is possible. By construction, it should leave the goal with + no remaining equalities generated by the [generalize_eqs] tactic. *) + +Ltac simplify_dep_elim := repeat simplify_one_dep_elim. + +(** To dependent elimination on some hyp. *) + +Ltac depelim id := + generalize_eqs id ; destruct id ; simplify_dep_elim. + +(** Do dependent elimination of the last hypothesis, but not simplifying yet + (used internally). *) + +Ltac destruct_last := + on_last_hyp ltac:(fun id => simpl in id ; generalize_eqs id ; destruct id). + +(** The rest is support tactics for the [Equations] command. *) + +(** Notation for inaccessible patterns. *) + +Definition inaccessible_pattern {A : Type} (t : A) := t. + +Notation "?( t )" := (inaccessible_pattern t). + +(** To handle sections, we need to separate the context in two parts: + variables introduced by the section and the rest. We introduce a dummy variable + between them to indicate that. *) + +CoInductive end_of_section := the_end_of_the_section. + +Ltac set_eos := let eos := fresh "eos" in + assert (eos:=the_end_of_the_section). + +(** We have a specialized [reverse_local] tactic to reverse the goal until the begining of the + section variables *) + +Ltac reverse_local := + match goal with + | [ H : ?T |- _ ] => + match T with + | end_of_section => idtac | _ => revert H ; reverse_local end + | _ => idtac + end. + +(** Do as much as possible to apply a method, trying to get the arguments right. + !!Unsafe!! We use [auto] for the [_nocomp] variant of [Equations], in which case some + non-dependent arguments of the method can remain after [apply]. *) + +Ltac simpl_intros m := ((apply m || refine m) ; auto) || (intro ; simpl_intros m). + +(** Hopefully the first branch suffices. *) + +Ltac try_intros m := + solve [ intros ; unfold block_dep_elim ; refine m || apply m ] || + solve [ unfold block_dep_elim ; simpl_intros m ]. + +(** To solve a goal by inversion on a particular target. *) + +Ltac solve_empty target := + do_nat target intro ; elimtype False ; destruct_last ; simplify_dep_elim. + +Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local. + +(** Solving a method call: we can solve it by splitting on an empty family member + or we must refine the goal until the body can be applied. *) + +Ltac solve_method rec := + match goal with + | [ H := ?body : nat |- _ ] => subst H ; clear ; abstract (simplify_method idtac ; solve_empty body) + | [ H := [ ?body ] : ?T |- _ ] => clear H ; simplify_method ltac:(exact body) ; rec ; try_intros (body:T) + end. + +(** Impossible cases, by splitting on a given target. *) + +Ltac solve_split := + match goal with + | [ |- let split := ?x : nat in _ ] => clear ; abstract (intros _ ; solve_empty x) + end. + +(** If defining recursive functions, the prototypes come first. *) + +Ltac intro_prototypes := + match goal with + | [ |- Π x : _, _ ] => intro ; intro_prototypes + | _ => idtac + end. + +Ltac do_case p := destruct p || elim_case p || (case p ; clear p). +Ltac do_ind p := induction p || elim_ind p. + +Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end. + +Ltac un_dep_elimify := unfold block_dep_elim in *. + +Ltac case_last := dep_elimify ; + on_last_hyp ltac:(fun p => + let ty := type of p in + match ty with + | ?x = ?x => revert p ; refine (simplification_K _ x _ _) + | ?x = ?y => revert p + | _ => simpl in p ; generalize_eqs p ; do_case p + end). + +Ltac nonrec_equations := + solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ] + || fail "Unnexpected equations goal". + +Ltac recursive_equations := + solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ] + || fail "Unnexpected recursive equations goal". + +(** The [equations] tactic is the toplevel tactic for solving goals generated + by [Equations]. *) + +Ltac equations := set_eos ; + match goal with + | [ |- Π x : _, _ ] => intro ; recursive_equations + | _ => nonrec_equations + end. + (** The following tactics allow to do induction on an already instantiated inductive predicate by first generalizing it and adding the proper equalities to the context, in a maner similar to the BasicElim tactic of "Elimination with a motive" by Conor McBride. *) @@ -235,43 +520,49 @@ Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; and starts a dependent induction using this tactic. *) Ltac do_depind tac H := - generalize_eqs_vars H ; tac H ; repeat progress simpl_depind. + (try intros until H) ; dep_elimify ; generalize_eqs_vars H ; tac H ; simplify_dep_elim ; un_dep_elimify. (** A variant where generalized variables should be given by the user. *) Ltac do_depind' tac H := - generalize_eqs H ; tac H ; repeat progress simpl_depind. + (try intros until H) ; dep_elimify ; generalize_eqs H ; tac H ; simplify_dep_elim ; un_dep_elimify. -(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *) +(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. + By default, we don't try to generalize the hyp by its variable indices. *) Tactic Notation "dependent" "destruction" ident(H) := - do_depind ltac:(fun hyp => destruct hyp ; intros) H ; subst*. + do_depind' ltac:(fun hyp => do_case hyp) H. Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := - do_depind ltac:(fun hyp => destruct hyp using c ; intros) H. + do_depind' ltac:(fun hyp => destruct hyp using c) H. (** This tactic also generalizes the goal by the given variables before the induction. *) Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := - do_depind' ltac:(fun hyp => revert l ; destruct hyp ; intros) H. + do_depind' ltac:(fun hyp => revert l ; do_case hyp) H. Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := - do_depind' ltac:(fun hyp => revert l ; destruct hyp using c ; intros) H. + do_depind' ltac:(fun hyp => revert l ; destruct hyp using c) H. (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by - writting another wrapper calling do_depind. *) + writting another wrapper calling do_depind. We suppose the hyp has to be generalized before + calling [induction]. *) Tactic Notation "dependent" "induction" ident(H) := - do_depind ltac:(fun hyp => induction hyp ; intros) H. + do_depind ltac:(fun hyp => do_ind hyp) H. Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := - do_depind ltac:(fun hyp => induction hyp using c ; intros) H. + do_depind ltac:(fun hyp => induction hyp using c) H. (** This tactic also generalizes the goal by the given variables before the induction. *) Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := - do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp ; intros) H. + do_depind' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H. Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := - do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c ; intros) H. + do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H. +Ltac simplify_IH_hyps := repeat + match goal with + | [ hyp : _ |- _ ] => specialize_hypothesis hyp + end.
\ No newline at end of file diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v deleted file mode 100644 index b5ad5b4d..00000000 --- a/theories/Program/FunctionalExtensionality.v +++ /dev/null @@ -1,109 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: FunctionalExtensionality.v 10739 2008-04-01 14:45:20Z herbelin $ i*) - -(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. - It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. - - It also defines two lemmas for expansion of fixpoint defs using extensionnality and proof-irrelevance - to avoid a side condition on the functionals. *) - -Require Import Coq.Program.Utils. -Require Import Coq.Program.Wf. -Require Import Coq.Program.Equality. - -Set Implicit Arguments. -Unset Strict Implicit. - -(** The converse of functional equality. *) - -Lemma equal_f : forall A B : Type, forall (f g : A -> B), - f = g -> forall x, f x = g x. -Proof. - intros. - rewrite H. - auto. -Qed. - -(** Statements of functional equality for simple and dependent functions. *) - -Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), - forall (f g : forall x : A, B x), - (forall x, f x = g x) -> f = g. - -Lemma fun_extensionality : forall A B (f g : A -> B), - (forall x, f x = g x) -> f = g. -Proof. - intros ; apply fun_extensionality_dep. - assumption. -Qed. - -Hint Resolve fun_extensionality fun_extensionality_dep : program. - -(** Apply [fun_extensionality], introducing variable x. *) - -Tactic Notation "extensionality" ident(x) := - match goal with - [ |- ?X = ?Y ] => apply (@fun_extensionality _ _ X Y) || apply (@fun_extensionality_dep _ _ X Y) ; intro x - end. - -(** Eta expansion follows from extensionality. *) - -Lemma eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), - f = fun x => f x. -Proof. - intros. - extensionality x. - reflexivity. -Qed. - -Lemma eta_expansion : forall A B (f : A -> B), - f = fun x => f x. -Proof. - intros ; apply eta_expansion_dep. -Qed. - -(** The two following lemmas allow to unfold a well-founded fixpoint definition without - restriction using the functional extensionality axiom. *) - -(** For a function defined with Program using a well-founded order. *) - -Program Lemma fix_sub_eq_ext : - forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) - (P : A -> Set) - (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), - forall x : A, - Fix_sub A R Rwf P F_sub x = - F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y). -Proof. - intros ; apply Fix_eq ; auto. - intros. - assert(f = g). - extensionality y ; apply H. - rewrite H0 ; auto. -Qed. - -(** For a function defined with Program using a measure. *) - -Program Lemma fix_sub_measure_eq_ext : - forall (A : Type) (f : A -> nat) (P : A -> Type) - (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x), - forall x : A, - Fix_measure_sub A f P F_sub x = - F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y). -Proof. - intros ; apply Fix_measure_eq ; auto. - intros. - assert(f0 = g). - extensionality y ; apply H. - rewrite H0 ; auto. -Qed. - - diff --git a/theories/Program/Program.v b/theories/Program/Program.v index b6c3031e..7d0c3948 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,3 +1,12 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* $Id: Program.v 11709 2008-12-20 11:42:15Z msozeau $ *) + Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. Require Export Coq.Program.Equality. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index d021326a..3d551281 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -5,14 +5,15 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id: Subset.v 11709 2008-12-20 11:42:15Z msozeau $ *) + +(** Tactics related to subsets and proof irrelevance. *) Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. Open Local Scope program_scope. -(** Tactics related to subsets and proof irrelevance. *) - (** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 6cd75257..222b5c8d 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,14 +5,15 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id: Syntax.v 11823 2009-01-21 15:32:37Z msozeau $ *) -(* Custom notations and implicits for Coq prelude definitions. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** Custom notations and implicits for Coq prelude definitions. -(** Notations for the unit type and value. *) + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) + +(** Notations for the unit type and value à la Haskell. *) Notation " () " := Datatypes.unit : type_scope. Notation " () " := tt. @@ -42,7 +42,7 @@ Notation " [ ] " := nil : list_scope. Notation " [ x ] " := (cons x nil) : list_scope. Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. -(** n-ary exists *) +(** Treating n-ary exists *) Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) (at level 200, x ident, y ident, right associativity) : type_scope. @@ -53,7 +53,7 @@ Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p))) Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p)))))))) (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope. -Tactic Notation "exist" constr(x) := exists x. -Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y. -Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. -Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. +Tactic Notation "exists" constr(x) := exists x. +Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y. +Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. +Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index bb5054b4..499629a6 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,11 +6,24 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: Tactics.v 11709 2008-12-20 11:42:15Z msozeau $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) +(** The [do] tactic but using a Coq-side nat. *) + +Ltac do_nat n tac := + match n with + | 0 => idtac + | S ?n' => tac ; do_nat n' tac + end. + +(** Do something on the last hypothesis, or fail *) + +Ltac on_last_hyp tac := + match goal with [ H : _ |- _ ] => tac H || fail 1 end. + (** Destructs one pair, without care regarding naming. *) Ltac destruct_one_pair := @@ -80,7 +93,7 @@ Ltac clear_dup := | [ H' : ?Y |- _ ] => match H with | H' => fail 2 - | _ => conv X Y ; (clear H' || clear H) + | _ => unify X Y ; (clear H' || clear H) end end end. @@ -91,7 +104,7 @@ Ltac clear_dups := repeat clear_dup. Ltac subst_no_fail := repeat (match goal with - [ H : ?X = ?Y |- _ ] => subst X || subst Y + [ H : ?X = ?Y |- _ ] => subst X || subst Y end). Tactic Notation "subst" "*" := subst_no_fail. @@ -108,6 +121,26 @@ Ltac on_application f tac T := | context [f ?x ?y] => tac (f x y) | context [f ?x] => tac (f x) end. + +(** A variant of [apply] using [refine], doing as much conversion as necessary. *) + +Ltac rapply p := + refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _ _) || + refine (p _ _ _ _ _ _) || + refine (p _ _ _ _ _) || + refine (p _ _ _ _) || + refine (p _ _ _) || + refine (p _ _) || + refine (p _) || + refine p. (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *) @@ -154,13 +187,14 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(i (** Try to inject any potential constructor equality hypothesis. *) -Ltac autoinjection := - let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in - match goal with - | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H - end. +Ltac autoinjection tac := + match goal with + | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H + end. + +Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H. -Ltac autoinjections := repeat autoinjection. +Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject). (** Destruct an hypothesis by first copying it to avoid dependencies. *) diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index fcd85f41..b08093bf 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Utils.v 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: Utils.v 11709 2008-12-20 11:42:15Z msozeau $ i*) + +(** Various syntaxic shortands that are useful with [Program]. *) Require Export Coq.Program.Tactics. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index b6ba5d44..12bdf3a7 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -1,3 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* $Id: Wf.v 11709 2008-12-20 11:42:15Z msozeau $ *) + +(** Reformulation of the Wf module using subsets where possible, providing + the support for [Program]'s treatment of well-founded definitions. *) + Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. @@ -6,8 +18,6 @@ Open Local Scope program_scope. Implicit Arguments Acc_inv [A R x y]. -(** Reformulation of the Wellfounded module using subsets where possible. *) - Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. @@ -146,3 +156,196 @@ Section Well_founded_measure. End Well_founded_measure. Extraction Inline Fix_measure_F_sub Fix_measure_sub. + +Set Implicit Arguments. + +(** Reasoning about well-founded fixpoints on measures. *) + +Section Measure_well_founded. + + (* Measure relations are well-founded if the underlying relation is well-founded. *) + + Variables T M: Set. + Variable R: M -> M -> Prop. + Hypothesis wf: well_founded R. + Variable m: T -> M. + + Definition MR (x y: T): Prop := R (m x) (m y). + + Lemma measure_wf: well_founded MR. + Proof with auto. + unfold well_founded. + cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a). + intros. + apply (H (m a))... + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). + intros. + apply Acc_intro. + intros. + unfold MR in H1. + rewrite H0 in H1. + apply (H (m y))... + Defined. + +End Measure_well_founded. + +Section Fix_measure_rects. + + Variable A: Set. + Variable m: A -> nat. + Variable P: A -> Type. + Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x. + + Lemma F_unfold x r: + Fix_measure_F_sub A m P f x r = + f (fun y => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv r (proj2_sig y))). + Proof. intros. case r; auto. Qed. + + (* Fix_measure_F_sub_rect lets one prove a property of + functions defined using Fix_measure_F_sub by showing + that property to be invariant over single application of the + function body (f in our case). *) + + Lemma Fix_measure_F_sub_rect + (Q: forall x, P x -> Type) + (inv: forall x: A, + (forall (y: A) (H: MR lt m y x) (a: Acc lt (m y)), + Q y (Fix_measure_F_sub A m P f y a)) -> + forall (a: Acc lt (m x)), + Q x (f (fun y: {y: A | m y < m x} => + Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y))))) + : forall x a, Q _ (Fix_measure_F_sub A m P f x a). + Proof with auto. + intros Q inv. + set (R := fun (x: A) => forall a, Q _ (Fix_measure_F_sub A m P f x a)). + cut (forall x, R x)... + apply (well_founded_induction_type (measure_wf lt_wf m)). + subst R. + simpl. + intros. + rewrite F_unfold... + Qed. + + (* Let's call f's second parameter its "lowers" function, since it + provides it access to results for inputs with a lower measure. + + In preparation of lemma similar to Fix_measure_F_sub_rect, but + for Fix_measure_sub, we first + need an extra hypothesis stating that the function body has the + same result for different "lowers" functions (g and h below) as long + as those produce the same results for lower inputs, regardless + of the lt proofs. *) + + Hypothesis equiv_lowers: + forall x0 (g h: forall x: {y: A | m y < m x0}, P (proj1_sig x)), + (forall x p p', g (exist (fun y: A => m y < m x0) x p) = h (exist _ x p')) -> + f g = f h. + + (* From equiv_lowers, it follows that + [Fix_measure_F_sub A m P f x] applications do not not + depend on the Acc proofs. *) + + Lemma eq_Fix_measure_F_sub x (a a': Acc lt (m x)): + Fix_measure_F_sub A m P f x a = + Fix_measure_F_sub A m P f x a'. + Proof. + intros x a. + pattern x, (Fix_measure_F_sub A m P f x a). + apply Fix_measure_F_sub_rect. + intros. + rewrite F_unfold. + apply equiv_lowers. + intros. + apply H. + assumption. + Qed. + + (* Finally, Fix_measure_F_rect lets one prove a property of + functions defined using Fix_measure_F by showing that + property to be invariant over single application of the function + body (f). *) + + Lemma Fix_measure_sub_rect + (Q: forall x, P x -> Type) + (inv: forall + (x: A) + (H: forall (y: A), MR lt m y x -> Q y (Fix_measure_sub A m P f y)) + (a: Acc lt (m x)), + Q x (f (fun y: {y: A | m y < m x} => Fix_measure_sub A m P f (proj1_sig y)))) + : forall x, Q _ (Fix_measure_sub A m P f x). + Proof with auto. + unfold Fix_measure_sub. + intros. + apply Fix_measure_F_sub_rect. + intros. + assert (forall y: A, MR lt m y x0 -> Q y (Fix_measure_F_sub A m P f y (lt_wf (m y))))... + set (inv x0 X0 a). clearbody q. + rewrite <- (equiv_lowers (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (lt_wf (m (proj1_sig y)))) (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... + intros. + apply eq_Fix_measure_F_sub. + Qed. + +End Fix_measure_rects. + +(** Tactic to fold a definitions based on [Fix_measure_sub]. *) + +Ltac fold_sub f := + match goal with + | [ |- ?T ] => + match T with + appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => + let app := context C [ f arg ] in + change app + end + end. + +(** This module provides the fixpoint equation provided one assumes + functional extensionality. *) + +Module WfExtensionality. + + Require Import FunctionalExtensionality. + + (** The two following lemmas allow to unfold a well-founded fixpoint definition without + restriction using the functional extensionality axiom. *) + + (** For a function defined with Program using a well-founded order. *) + + Program Lemma fix_sub_eq_ext : + forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) + (P : A -> Set) + (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), + forall x : A, + Fix_sub A R Rwf P F_sub x = + F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y). + Proof. + intros ; apply Fix_eq ; auto. + intros. + assert(f = g). + extensionality y ; apply H. + rewrite H0 ; auto. + Qed. + + (** For a function defined with Program using a measure. *) + + Program Lemma fix_sub_measure_eq_ext : + forall (A : Type) (f : A -> nat) (P : A -> Type) + (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x), + forall x : A, + Fix_measure_sub A f P F_sub x = + F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y). + Proof. + intros ; apply Fix_measure_eq ; auto. + intros. + assert(f0 = g). + extensionality y ; apply H. + rewrite H0 ; auto. + Qed. + + (** Tactic to unfold once a definition based on [Fix_measure_sub]. *) + + Ltac unfold_sub f fargs := + set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; + rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig. + +End WfExtensionality. |