diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Basics.v | 16 | ||||
| -rw-r--r-- | theories/Program/Combinators.v | 11 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 397 | ||||
| -rw-r--r-- | theories/Program/Program.v | 2 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 30 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 19 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 106 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 2 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 305 | ||||
| -rw-r--r-- | theories/Program/vo.itarget | 9 |
10 files changed, 382 insertions, 515 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 29494069..0a4b15d2 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -5,15 +6,16 @@ (* // * 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 $ *) +(* $Id$ *) (** Standard functions and combinators. - - Proofs about them require functional extensionality and can be found in [Combinators]. + + Proofs about them require functional extensionality and can be found + in [Combinators]. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Université Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (** The polymorphic identity function is defined in [Datatypes]. *) @@ -21,12 +23,12 @@ Implicit Arguments id [[A]]. (** Function composition. *) -Definition compose {A B C} (g : B -> C) (f : A -> B) := +Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x : A => g (f x). Hint Unfold compose. -Notation " g ∘ f " := (compose g f) +Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : program_scope. Open Local Scope program_scope. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index ae9749de..31661b9d 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -5,13 +6,13 @@ (* // * 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 $ *) +(* $Id$ *) -(** Proofs about standard combinators, exports functional extensionality. +(** * Proofs about standard combinators, exports functional extensionality. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) Require Import Coq.Program.Basics. Require Export FunctionalExtensionality. @@ -34,7 +35,7 @@ Proof. symmetry ; apply eta_expansion. Qed. -Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), +Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), h ∘ g ∘ f = h ∘ (g ∘ f). Proof. intros. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 9681d543..79c9bec5 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,4 +1,3 @@ -(* -*- 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 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 12073 2009-04-08 21:04:42Z msozeau $ i*) +(*i $Id$ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -16,17 +15,35 @@ Require Export JMeq. Require Import Coq.Program.Tactics. +Ltac is_ground_goal := + match goal with + |- ?T => is_ground T + end. + +(** Try to find a contradiction. *) + +Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. + +(** We will use the [block] definition to separate the goal from the + equalities generated by the tactic. *) + +Definition block {A : Type} (a : A) := a. + +Ltac block_goal := match goal with [ |- ?T ] => change (block T) end. +Ltac unblock_goal := unfold block in *. + (** Notation for heterogenous equality. *) -Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level). +Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). -(** Notation for the single element of [x = x] *) +(** Notation for the single element of [x = x] and [x ~= x]. *) -Notation "'refl'" := (@refl_equal _ _). +Implicit Arguments eq_refl [[A] [x]]. +Implicit Arguments JMeq_refl [[A] [x]]. (** Do something on an heterogeneous equality appearing in the context. *) -Ltac on_JMeq tac := +Ltac on_JMeq tac := match goal with | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H end. @@ -44,17 +61,17 @@ Ltac simpl_JMeq := repeat simpl_one_JMeq. Ltac simpl_one_dep_JMeq := on_JMeq - ltac:(fun H => let H' := fresh "H" in + ltac:(fun H => let H' := fresh "H" in assert (H' := JMeq_eq H)). Require Import Eqdep. -(** Simplify dependent equality using sigmas to equality of the second projections if possible. +(** Simplify dependent equality using sigmas to equality of the second projections if possible. Uses UIP. *) Ltac simpl_existT := match goal with - [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => + [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H end. @@ -64,20 +81,20 @@ Ltac simpl_existTs := repeat simpl_existT. Ltac elim_eq_rect := match goal with - | [ |- ?t ] => + | [ |- ?t ] => match t with - | context [ @eq_rect _ _ _ _ _ ?p ] => - let P := fresh "P" in - set (P := p); simpl in P ; + | context [ @eq_rect _ _ _ _ _ ?p ] => + let P := fresh "P" in + set (P := p); simpl in P ; ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - | context [ @eq_rect _ _ _ _ _ ?p _ ] => - let P := fresh "P" in - set (P := p); simpl in P ; + | context [ @eq_rect _ _ _ _ _ ?p _ ] => + let P := fresh "P" in + set (P := p); simpl in P ; ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) end end. -(** Rewrite using uniqueness of indentity proofs [H = refl_equal X]. *) +(** Rewrite using uniqueness of indentity proofs [H = eq_refl]. *) Ltac simpl_uip := match goal with @@ -90,18 +107,18 @@ Ltac simpl_eq := simpl ; unfold eq_rec_r, eq_rec ; repeat (elim_eq_rect ; simpl) (** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *) -Ltac abstract_eq_hyp H' p := +Ltac abstract_eq_hyp H' p := let ty := type of p in let tyred := eval simpl in ty in - match tyred with - ?X = ?Y => - match goal with + match tyred with + ?X = ?Y => + match goal with | [ H : X = Y |- _ ] => fail 1 | _ => set (H':=p) ; try (change p with H') ; clearbody H' ; simpl in H' end end. -(** Apply the tactic tac to proofs of equality appearing as coercion arguments. +(** Apply the tactic tac to proofs of equality appearing as coercion arguments. Just redefine this tactic (using [Ltac on_coerce_proof tac ::=]) to handle custom coercion operators. *) @@ -109,7 +126,7 @@ Ltac on_coerce_proof tac T := match T with | context [ eq_rect _ _ _ _ ?p ] => tac p end. - + Ltac on_coerce_proof_gl tac := match goal with [ |- ?T ] => on_coerce_proof tac T @@ -120,17 +137,17 @@ Ltac on_coerce_proof_gl tac := Ltac abstract_eq_proof := on_coerce_proof_gl ltac:(fun p => let H := fresh "eqH" in abstract_eq_hyp H p). Ltac abstract_eq_proofs := repeat abstract_eq_proof. - -(** Factorize proofs, by using proof irrelevance so that two proofs of the same equality + +(** Factorize proofs, by using proof irrelevance so that two proofs of the same equality in the goal become convertible. *) Ltac pi_eq_proof_hyp p := let ty := type of p in let tyred := eval simpl in ty in match tyred with - ?X = ?Y => - match goal with - | [ H : X = Y |- _ ] => + ?X = ?Y => + match goal with + | [ H : X = Y |- _ ] => match p with | H => fail 2 | _ => rewrite (proof_irrelevance (X = Y) p H) @@ -152,8 +169,21 @@ Ltac clear_eq_proofs := Hint Rewrite <- eq_rect_eq : refl_id. -(** The refl_id database should be populated with lemmas of the form - [coerce_* t (refl_equal _) = t]. *) +(** The [refl_id] database should be populated with lemmas of the form + [coerce_* t eq_refl = t]. *) + +Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl. +Proof. intros. apply proof_irrelevance. Qed. + +Lemma UIP_refl_refl : Π A (x : A), + Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl. +Proof. intros. apply UIP_refl. Qed. + +Lemma inj_pairT2_refl : Π A (x : A) (P : A -> Type) (p : P x), + Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl. +Proof. intros. apply UIP_refl. Qed. + +Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. Ltac rewrite_refl_id := autorewrite with refl_id. @@ -162,82 +192,49 @@ Ltac rewrite_refl_id := autorewrite with refl_id. Ltac clear_eq_ctx := rewrite_refl_id ; clear_eq_proofs. -(** Reapeated elimination of [eq_rect] applications. +(** Reapeated elimination of [eq_rect] applications. Abstracting equalities makes it run much faster than an naive implementation. *) -Ltac simpl_eqs := +Ltac simpl_eqs := repeat (elim_eq_rect ; simpl ; clear_eq_ctx). (** Clear unused reflexivity proofs. *) -Ltac clear_refl_eq := +Ltac clear_refl_eq := match goal with [ H : ?X = ?X |- _ ] => clear H end. Ltac clear_refl_eqs := repeat clear_refl_eq. (** Clear unused equality proofs. *) -Ltac clear_eq := +Ltac clear_eq := match goal with [ H : _ = _ |- _ ] => clear H end. Ltac clear_eqs := repeat clear_eq. (** Combine all the tactics to simplify goals containing coercions. *) -Ltac simplify_eqs := - simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ; +Ltac simplify_eqs := + simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ; try subst ; simpl ; repeat simpl_uip ; rewrite_refl_id. (** 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 _ _ -> _ => - refine_hyp (H (JMeq_refl x)) - | _ -> @JMeq _ ?x _ _ -> _ => - refine_hyp (H _ (JMeq_refl x)) - | _ -> _ -> @JMeq _ ?x _ _ -> _ => - refine_hyp (H _ _ (JMeq_refl x)) - | _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => - refine_hyp (H _ _ _ (JMeq_refl x)) - | _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => - refine_hyp (H _ _ _ _ (JMeq_refl x)) - | _ -> _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => - refine_hyp (H _ _ _ _ _ (JMeq_refl x)) - | ?x = _ -> _ => - refine_hyp (H (refl_equal x)) - | _ -> ?x = _ -> _ => - refine_hyp (H _ (refl_equal x)) - | _ -> _ -> ?x = _ -> _ => - refine_hyp (H _ _ (refl_equal x)) - | _ -> _ -> _ -> ?x = _ -> _ => - refine_hyp (H _ _ _ (refl_equal x)) - | _ -> _ -> _ -> _ -> ?x = _ -> _ => - refine_hyp (H _ _ _ _ (refl_equal x)) - | _ -> _ -> _ -> _ -> _ -> ?x = _ -> _ => - refine_hyp (H _ _ _ _ _ (refl_equal x)) - end. - -Ltac simpl_IH_eqs H := repeat simpl_IH_eq H. - -Ltac do_simpl_IHs_eqs := +Ltac simplify_IH_hyps := repeat match goal with - | [ H : context [ @JMeq _ _ _ _ -> _ ] |- _ ] => progress (simpl_IH_eqs H) - | [ H : context [ _ = _ -> _ ] |- _ ] => progress (simpl_IH_eqs H) + | [ hyp : _ |- _ ] => specialize_eqs hyp end. -Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs. - (** 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 + repeat (match goal with [ H : ?X = ?Y |- _ ] => subst X end). Ltac subst_right_no_fail := - repeat (match goal with + repeat (match goal with [ H : ?X = ?Y |- _ ] => subst Y end). @@ -251,32 +248,15 @@ 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. + simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ; - simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs. + simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. 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 }. + simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. + +Ltac blocked t := block_goal ; t ; unblock_goal. (** The [DependentEliminationPackage] provides the default dependent elimination principle to be used by the [equations] resolver. It is especially useful to register the dependent elimination @@ -287,30 +267,18 @@ Class DependentEliminationPackage (A : Type) := (** A higher-order tactic to apply a registered eliminator. *) -Ltac elim_tac tac p := +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 +(** 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). @@ -333,57 +301,43 @@ Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P (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). +Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B eq_refl -> (Π 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 +(** This hint database and the following tactic can be used with [autounfold] 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. + simplification_existT1 simplification_existT2 simplification_K + eq_rect_r eq_rec eq_ind : dep_elim. -(** Using these we can make a simplifier that will perform the unification +(** 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. *) + 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 _ _ _) -> _ => + | 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) || + move hyp before x ; revert_until hyp ; 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) + move hyp before y ; revert_until hyp ; generalize dependent y ; + refine (solution_right _ _ _ _)(* ; intros until 0 *)) | ?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 + intros hyp ; exfalso ; 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 *) + | block ?T => fail 1 (* Do not put any part of the rhs in the hyps *) + | forall x, _ => intro x || (let H := fresh x in rename x into H ; intro x) (* Try to keep original names *) | _ => intro end. @@ -397,176 +351,103 @@ Ltac simplify_one_dep_elim := 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). +Ltac introduce p := first [ + match p with _ => (* Already there, generalize dependent hyps *) + generalize dependent p ; intros p + end + | intros until p | intros until 1 | intros ]. -(** 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 do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)). +Ltac do_ind p := introduce p ; (induction p || elim_ind p). -Ltac solve_empty target := - do_nat target intro ; elimtype False ; destruct_last ; simplify_dep_elim. +(** 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. *) -Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local. +(** The [do_depelim] higher-order tactic takes an elimination tactic as argument and an hypothesis + and starts a dependent elimination using this tactic. *) -(** 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 := +Ltac is_introduced H := 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) + | [ H' : _ |- _ ] => match H' with H => idtac end 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. +Tactic Notation "intro_block" hyp(H) := + (is_introduced H ; block_goal ; revert_until H) || + (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). -(** If defining recursive functions, the prototypes come first. *) +Tactic Notation "intro_block_id" ident(H) := + (is_introduced H ; block_goal ; revert_until H) || + (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). -Ltac intro_prototypes := - match goal with - | [ |- Π x : _, _ ] => intro ; intro_prototypes - | _ => idtac - end. - -Ltac introduce p := - first [ match p with _ => idtac end (* Already there *) - | intros until p | intros ]. - -Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)). -Ltac do_ind p := introduce p ; (induction p || elim_ind p). +Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. -Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end. +Ltac do_intros H := + (try intros until H) ; (intro_block_id H || intro_block H). -Ltac un_dep_elimify := unfold block_dep_elim in *. +Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; tac H. -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 do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim. -Ltac nonrec_equations := - solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ] - || fail "Unnexpected equations goal". +Ltac do_depind tac H := + (try intros until H) ; intro_block H ; + generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. -Ltac recursive_equations := - solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ] - || fail "Unnexpected recursive equations goal". +(** To dependent elimination on some hyp. *) -(** The [equations] tactic is the toplevel tactic for solving goals generated - by [Equations]. *) +Ltac depelim id := do_depelim ltac:(fun hyp => do_case hyp) id. -Ltac equations := set_eos ; - match goal with - | [ |- Π x : _, _ ] => intro ; recursive_equations - | _ => nonrec_equations - end. +(** Used internally. *) -(** 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. *) +Ltac depelim_nosimpl id := do_depelim_nosimpl ltac:(fun hyp => do_case hyp) id. -(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis - and starts a dependent induction using this tactic. *) +(** To dependent induction on some hyp. *) -Ltac do_depind tac H := - (try intros until H) ; dep_elimify ; generalize_eqs_vars H ; tac H ; simplify_dep_elim ; un_dep_elimify. +Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id. (** A variant where generalized variables should be given by the user. *) -Ltac do_depind' tac H := - (try intros until H) ; dep_elimify ; generalize_eqs H ; tac H ; simplify_dep_elim ; un_dep_elimify. +Ltac do_depelim' tac H := + (try intros until H) ; block_goal ; generalize_eqs H ; tac H ; simplify_dep_elim ; + simplify_IH_hyps ; unblock_goal. (** 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 => do_case hyp) H. + do_depelim' 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) H. + do_depelim' ltac:(fun hyp => destruct hyp using c) H. -(** This tactic also generalizes the goal by the given variables before the induction. *) +(** This tactic also generalizes the goal by the given variables before the elimination. *) Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := - do_depind' ltac:(fun hyp => revert l ; do_case hyp) H. + do_depelim' 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) H. + do_depelim' 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. We suppose the hyp has to be generalized before + writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before calling [induction]. *) -Tactic Notation "dependent" "induction" ident(H) := +Tactic Notation "dependent" "induction" ident(H) := do_depind ltac:(fun hyp => do_ind hyp) H. -Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := +Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 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 ; do_ind hyp) H. + do_depelim' 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) H. - -Ltac simplify_IH_hyps := repeat - match goal with - | [ hyp : _ |- _ ] => specialize_hypothesis hyp - end.
\ No newline at end of file + do_depelim' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H. diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 7d0c3948..cdfc7858 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -5,7 +5,7 @@ (* // * 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 $ *) +(* $Id$ *) Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 3d551281..89f477d8 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -5,7 +5,7 @@ (* // * 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 $ *) +(* $Id$ *) (** Tactics related to subsets and proof irrelevance. *) @@ -14,7 +14,7 @@ Require Import Coq.Program.Equality. Open Local Scope program_scope. -(** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to +(** 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. *) Ltac on_subset_proof_aux tac T := @@ -27,25 +27,25 @@ Ltac on_subset_proof tac := [ |- ?T ] => on_subset_proof_aux tac T end. -Ltac abstract_any_hyp H' p := +Ltac abstract_any_hyp H' p := match type of p with - ?X => - match goal with + ?X => + match goal with | [ H : X |- _ ] => fail 1 | _ => set (H':=p) ; try (change p with H') ; clearbody H' end end. -Ltac abstract_subset_proof := +Ltac abstract_subset_proof := on_subset_proof ltac:(fun p => let H := fresh "eqH" in abstract_any_hyp H p ; simpl in H). Ltac abstract_subset_proofs := repeat abstract_subset_proof. Ltac pi_subset_proof_hyp p := match type of p with - ?X => - match goal with - | [ H : X |- _ ] => + ?X => + match goal with + | [ H : X |- _ ] => match p with | H => fail 2 | _ => rewrite (proof_irrelevance X p H) @@ -78,16 +78,16 @@ Proof. pi. Qed. -(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] +(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] in tactics. *) Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B := - fn (exist _ x (refl_equal x)). + fn (exist _ x eq_refl). -(* This is what we want to be able to do: replace the originaly matched object by a new, +(* This is what we want to be able to do: replace the originaly matched object by a new, propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *) -Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B) +Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B) (y : A | y = x), match_eq A B x fn = fn y. Proof. @@ -103,9 +103,9 @@ Qed. (** Now we make a tactic to be able to rewrite a term [t] which is applied to a [match_eq] using an arbitrary equality [t = u], and [u] is now the subject of the [match]. *) -Ltac rewrite_match_eq H := +Ltac rewrite_match_eq H := match goal with - [ |- ?T ] => + [ |- ?T ] => match T with context [ match_eq ?A ?B ?t ?f ] => rewrite (match_eq_rewrite A B t f (exist _ _ (sym_eq H))) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 222b5c8d..2064977f 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -5,15 +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 $ *) +(* $Id$ *) (** Custom notations and implicits for Coq prelude definitions. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) -(** Notations for the unit type and value à la Haskell. *) +(** Haskell-style notations for the unit type and value. *) Notation " () " := Datatypes.unit : type_scope. Notation " () " := tt. @@ -31,6 +31,10 @@ Implicit Arguments inr [[A] [B]]. Implicit Arguments left [[A] [B]]. Implicit Arguments right [[A] [B]]. +Implicit Arguments pair [[A] [B]]. +Implicit Arguments fst [[A] [B]]. +Implicit Arguments snd [[A] [B]]. + Require Import Coq.Lists.List. Implicit Arguments nil [[A]]. @@ -42,6 +46,13 @@ Notation " [ ] " := nil : list_scope. Notation " [ x ] " := (cons x nil) : list_scope. Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. +(** Implicit arguments for vectors. *) + +Require Import Bvector. + +Implicit Arguments Vnil [[A]]. +Implicit Arguments Vcons [[A] [n]]. + (** Treating n-ary exists *) Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 499629a6..e692876d 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,11 +6,32 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 11709 2008-12-20 11:42:15Z msozeau $ i*) +(*i $Id$ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) +(** Debugging tactics to show the goal during evaluation. *) + +Ltac show_goal := match goal with [ |- ?T ] => idtac T end. + +Ltac show_hyp id := + match goal with + | [ H := ?b : ?T |- _ ] => + match H with + | id => idtac id ":=" b ":" T + end + | [ H : ?T |- _ ] => + match H with + | id => idtac id ":" T + end + end. + +Ltac show_hyps := + try match reverse goal with + | [ H : ?T |- _ ] => show_hyp H ; fail + end. + (** The [do] tactic but using a Coq-side nat. *) Ltac do_nat n tac := @@ -22,7 +43,7 @@ Ltac do_nat n tac := (** Do something on the last hypothesis, or fail *) Ltac on_last_hyp tac := - match goal with [ H : _ |- _ ] => tac H || fail 1 end. + match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end. (** Destructs one pair, without care regarding naming. *) @@ -56,7 +77,7 @@ Ltac destruct_exists := repeat (destruct_one_ex). Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). -(** Destruct an existential hypothesis [t] keeping its name for the first component +(** Destruct an existential hypothesis [t] keeping its name for the first component and using [Ht] for the second *) Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. @@ -75,7 +96,7 @@ Ltac discriminates := (** Revert the last hypothesis. *) -Ltac revert_last := +Ltac revert_last := match goal with [ H : _ |- _ ] => revert H end. @@ -84,11 +105,20 @@ Ltac revert_last := Ltac reverse := repeat revert_last. +(** Reverse everything up to hypothesis id (not included). *) + +Ltac revert_until id := + on_last_hyp ltac:(fun id' => + match id' with + | id => idtac + | _ => revert id' ; revert_until id + end). + (** Clear duplicated hypotheses *) Ltac clear_dup := - match goal with - | [ H : ?X |- _ ] => + match goal with + | [ H : ?X |- _ ] => match goal with | [ H' : ?Y |- _ ] => match H with @@ -100,10 +130,20 @@ Ltac clear_dup := Ltac clear_dups := repeat clear_dup. +(** Try to clear everything except some hyp *) + +Ltac clear_except hyp := + repeat match goal with [ H : _ |- _ ] => + match H with + | hyp => fail 1 + | _ => clear H + end + end. + (** A non-failing subst that substitutes as much as possible. *) Ltac subst_no_fail := - repeat (match goal with + repeat (match goal with [ H : ?X = ?Y |- _ ] => subst X || subst Y end). @@ -118,13 +158,13 @@ Ltac on_application f tac T := | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) | context [f ?x ?y ?z ?w] => tac (f x y z w) | context [f ?x ?y ?z] => tac (f x y z) - | context [f ?x ?y] => tac (f x y) + | 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 := +Ltac rapply p := refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) || refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) || @@ -141,7 +181,7 @@ Ltac rapply p := refine (p _ _) || refine (p _) || refine p. - + (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *) Ltac on_call f tac := @@ -174,17 +214,29 @@ Tactic Notation "destruct_call" constr(f) := destruct_call f. (** Permit to name the results of destructing the call to [f]. *) -Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := +Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l. (** Specify the hypothesis in which the call occurs as well. *) -Tactic Notation "destruct_call" constr(f) "in" hyp(id) := +Tactic Notation "destruct_call" constr(f) "in" hyp(id) := destruct_call_in f id. -Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) := +Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) := destruct_call_as_in f l id. +(** A marker for prototypes to destruct. *) + +Definition fix_proto {A : Type} (a : A) := a. + +Ltac destruct_rec_calls := + match goal with + | [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H + end. + +Ltac destruct_all_rec_calls := + repeat destruct_rec_calls ; unfold fix_proto in *. + (** Try to inject any potential constructor equality hypothesis. *) Ltac autoinjection tac := @@ -204,23 +256,23 @@ Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0. Ltac bang := match goal with - | |- ?x => + | |- ?x => match x with - | context [False_rect _ ?p] => elim p + | appcontext [False_rect _ ?p] => elim p end end. - + (** A tactic to show contradiction by first asserting an automatically provable hypothesis. *) -Tactic Notation "contradiction" "by" constr(t) := +Tactic Notation "contradiction" "by" constr(t) := let H := fresh in assert t as H by auto with * ; contradiction. (** A tactic that adds [H:=p:typeof(p)] to the context if no hypothesis of the same type appears in the goal. Useful to do saturation using tactics. *) -Ltac add_hypothesis H' p := +Ltac add_hypothesis H' p := match type of p with - ?X => - match goal with + ?X => + match goal with | [ H : X |- _ ] => fail 1 | _ => set (H':=p) ; try (change p with H') ; clearbody H' end @@ -248,13 +300,19 @@ Ltac refine_hyp c := end. (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto] - is not enough, better rebind using [Obligation Tactic := tac] in this case, + is not enough, better rebind using [Obligation Tactic := tac] in this case, possibly using [program_simplify] to use standard goal-cleaning tactics. *) Ltac program_simplify := - simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; autoinjections ; try discriminates ; + simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in *); + subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). -Ltac program_simpl := program_simplify ; auto. +Ltac program_solve_wf := + match goal with + |- well_founded _ => auto with * + end. + +Ltac program_simpl := program_simplify ; auto; try program_solve_wf. -Ltac obligation_tactic := program_simpl. +Obligation Tactic := program_simpl. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index b08093bf..fbf0b03c 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Utils.v 11709 2008-12-20 11:42:15Z msozeau $ i*) +(*i $Id$ i*) (** Various syntaxic shortands that are useful with [Program]. *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 2083e530..98b1c619 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Wf.v 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -22,140 +22,57 @@ Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. Hypothesis Rwf : well_founded R. - - Section Acc. - - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - - Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := - F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) - (Acc_inv r (proj2_sig y))). - - Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). - End Acc. - - Section FixPoint. - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - - Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) - - Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). - - Hypothesis - F_ext : - forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), - (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g. - - Lemma Fix_F_eq : - forall (x:A) (r:Acc R x), - F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r. - Proof. - destruct r using Acc_inv_dep; auto. - Qed. - - Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s. - Proof. - intro x; induction (Rwf x); intros. - rewrite (proof_irrelevance (Acc R x) r s) ; auto. - Qed. - - Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:A|R y x) => Fix (proj1_sig y)). - Proof. - intro x; unfold Fix in |- *. - rewrite <- (Fix_F_eq ). - apply F_ext; intros. - apply Fix_F_inv. - Qed. - - Lemma fix_sub_eq : - forall x : A, - Fix_sub P F_sub x = - let f_sub := F_sub in - f_sub x (fun (y : A | R y x) => Fix (`y)). - exact Fix_eq. - Qed. - - End FixPoint. -End Well_founded. + Variable P : A -> Type. -Extraction Inline Fix_F_sub Fix_sub. + Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. -Require Import Wf_nat. -Require Import Lt. + Fixpoint Fix_F_sub (x : A) (r : Acc R x) : P x := + F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) + (Acc_inv r (proj2_sig y))). -Section Well_founded_measure. - Variable A : Type. - Variable m : A -> nat. - - Section Acc. - - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. - - Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := - F_sub x (fun (y : A | m y < m x) => Fix_measure_F_sub y - (@Acc_inv _ _ _ r (m y) (proj2_sig y))). - - Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)). - - End Acc. - - Section FixPoint. - Variable P : A -> Type. - - Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x. - - Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *) - - Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)). - - Hypothesis - F_ext : - forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)), - (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. - - Program Lemma Fix_measure_F_eq : - forall (x:A) (r:Acc lt (m x)), - F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r. - Proof. - intros x. - set (y := m x). - unfold Fix_measure_F_sub. - intros r ; case r ; auto. - Qed. - - Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s. - Proof. - intros x r s. - rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto. - Qed. - - Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)). - Proof. - intro x; unfold Fix_measure in |- *. - rewrite <- (Fix_measure_F_eq ). - apply F_ext; intros. - apply Fix_measure_F_inv. - Qed. - - Lemma fix_measure_sub_eq : forall x : A, - Fix_measure_sub P F_sub x = - let f_sub := F_sub in - f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)). - exact Fix_measure_eq. - Qed. - - End FixPoint. - -End Well_founded_measure. - -Extraction Inline Fix_measure_F_sub Fix_measure_sub. + Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + + (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *) + (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *) + + Hypothesis + F_ext : + forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), + (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g. + + Lemma Fix_F_eq : + forall (x:A) (r:Acc R x), + F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. + Proof. + destruct r using Acc_inv_dep; auto. + Qed. + + Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s. + Proof. + intro x; induction (Rwf x); intros. + rewrite (proof_irrelevance (Acc R x) r s) ; auto. + Qed. + + Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)). + Proof. + intro x; unfold Fix_sub in |- *. + rewrite <- (Fix_F_eq ). + apply F_ext; intros. + apply Fix_F_inv. + Qed. + + Lemma fix_sub_eq : + forall x : A, + Fix_sub x = + let f_sub := F_sub in + f_sub x (fun (y : A | R y x) => Fix_sub (`y)). + exact Fix_eq. + Qed. + +End Well_founded. + +Extraction Inline Fix_F_sub Fix_sub. Set Implicit Arguments. @@ -189,38 +106,40 @@ Section Measure_well_founded. End Measure_well_founded. -Section Fix_measure_rects. +Hint Resolve measure_wf. + +Section Fix_rects. Variable A: Type. - 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. - + Variable R : A -> A -> Prop. + Variable Rwf : well_founded R. + Variable f: forall (x : A), (forall y: { y: A | R y 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))). + Fix_F_sub A R P f x r = + f (fun y => Fix_F_sub A R 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 + (* Fix_F_sub_rect lets one prove a property of + functions defined using Fix_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 + Lemma Fix_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). + (forall (y: A) (H: R y x) (a: Acc R y), + Q y (Fix_F_sub A R P f y a)) -> + forall (a: Acc R x), + Q x (f (fun y: {y: A | R y x} => + Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))) + : forall x a, Q _ (Fix_F_sub A R 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. + set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)). + cut (forall x, R' x)... + apply (well_founded_induction_type Rwf). + subst R'. simpl. intros. rewrite F_unfold... @@ -229,29 +148,29 @@ Section Fix_measure_rects. (* 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 + In preparation of lemma similar to Fix_F_sub_rect, but + for Fix_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')) -> + forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)), + (forall x p p', g (exist (fun y: A => R y 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 + [Fix_F_sub A R 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'. + Lemma eq_Fix_F_sub x (a a': Acc R x): + Fix_F_sub A R P f x a = + Fix_F_sub A R 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. + revert a'. + pattern x, (Fix_F_sub A R P f x a). + apply Fix_F_sub_rect. intros. rewrite F_unfold. apply equiv_lowers. @@ -260,40 +179,42 @@ Section Fix_measure_rects. assumption. Qed. - (* Finally, Fix_measure_F_rect lets one prove a property of - functions defined using Fix_measure_F by showing that + (* Finally, Fix_F_rect lets one prove a property of + functions defined using Fix_F_sub by showing that property to be invariant over single application of the function body (f). *) - Lemma Fix_measure_sub_rect + Lemma Fix_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). + (H: forall (y: A), R y x -> Q y (Fix_sub A R Rwf P f y)) + (a: Acc R x), + Q x (f (fun y: {y: A | R y x} => Fix_sub A R Rwf P f (proj1_sig y)))) + : forall x, Q _ (Fix_sub A R Rwf P f x). Proof with auto. - unfold Fix_measure_sub. + unfold Fix_sub. intros. - apply Fix_measure_F_sub_rect. + apply Fix_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))))... + assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf 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))))... + rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => + Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) + (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... intros. - apply eq_Fix_measure_F_sub. + apply eq_Fix_F_sub. Qed. -End Fix_measure_rects. +End Fix_rects. (** Tactic to fold a definition based on [Fix_measure_sub]. *) Ltac fold_sub f := match goal with - | [ |- ?T ] => + | [ |- ?T ] => match T with - appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => + appcontext C [ @Fix_sub _ _ _ _ ?arg ] => let app := context C [ f arg ] in change app end @@ -308,7 +229,7 @@ Module WfExtensionality. (** 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 : @@ -317,7 +238,7 @@ Module WfExtensionality. (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). + F_sub x (fun (y : A | R y x) => Fix_sub A R Rwf P F_sub y). Proof. intros ; apply Fix_eq ; auto. intros. @@ -326,26 +247,10 @@ Module WfExtensionality. 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. + (** Tactic to unfold once a definition based on [Fix_sub]. *) + + Ltac unfold_sub f fargs := + set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; + rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig. End WfExtensionality. diff --git a/theories/Program/vo.itarget b/theories/Program/vo.itarget new file mode 100644 index 00000000..864c815a --- /dev/null +++ b/theories/Program/vo.itarget @@ -0,0 +1,9 @@ +Basics.vo +Combinators.vo +Equality.vo +Program.vo +Subset.vo +Syntax.vo +Tactics.vo +Utils.vo +Wf.vo |