diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-28 22:51:46 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-28 22:51:46 +0000 |
commit | 1cd1801ee86d6be178f5bce700633aee2416d236 (patch) | |
tree | 66020b29fd37f2471afc32ba8624bfa373db64b7 /theories/Program | |
parent | d491c4974ad7ec82a5369049c27250dd07de852c (diff) |
Integrate a few improvements on typeclasses and Program from the equations branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Equality.v | 339 | ||||
-rw-r--r-- | theories/Program/Subset.v | 2 | ||||
-rw-r--r-- | theories/Program/Syntax.v | 7 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 21 |
4 files changed, 139 insertions, 230 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 0c77a1325..76dc09b26 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,4 +1,3 @@ -(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -16,13 +15,31 @@ 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 (elimtype False). + +(** 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. *) @@ -77,7 +94,7 @@ Ltac elim_eq_rect := 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 @@ -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. @@ -189,45 +219,12 @@ 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 _ _ -> _ => - 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_hypothesis hyp end. -Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs. - -(** We split substitution tactics in the two directions depending on which +(** 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. *) @@ -250,33 +247,16 @@ Ltac inject_right 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 := subst_no_fail ; autoinjections ; try discriminates ; + 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. +Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ; + simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. -(** 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. *) +Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ; + simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. - -(** 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 }. +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 @@ -299,18 +279,6 @@ Ltac elim_tac tac p := 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). @@ -332,25 +300,16 @@ 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). + +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. -(** Simply unfold as much as possible. *) - -Ltac unfold_equations := - unfold solution_left, solution_right, deletion, simplification_heq, - simplification_existT1, simplification_existT2, eq_rect_r, eq_rec, eq_ind. - -(** 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. *) +(** This hint database and the following tactic can be used with [autounfold] to + unfold everything to [eq_rect]s. *) -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. +Hint Unfold solution_left solution_right deletion simplification_heq + 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 steps needed to put the goal in normalised form (provided there are only @@ -366,19 +325,18 @@ Ltac simplify_one_dep_elim_term c := 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 ; 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. @@ -393,161 +351,91 @@ 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). - -(** 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 ; exfalso ; destruct_last ; simplify_dep_elim. - -Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local. +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 ]. -(** 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 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_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. +(** 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. *) -(** Impossible cases, by splitting on a given target. *) +(** The [do_depelim] higher-order tactic takes an elimination tactic as argument and an hypothesis + and starts a dependent elimination using this tactic. *) -Ltac solve_split := +Ltac is_introduced H := match goal with - | [ |- let split := ?x : nat in _ ] => clear ; abstract (intros _ ; solve_empty x) + | [ H' : _ |- _ ] => match H' with H => idtac end end. -(** If defining recursive functions, the prototypes come first. *) +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). -Ltac intro_prototypes := - match goal with - | [ |- Π x : _, _ ] => intro ; intro_prototypes - | _ => idtac - end. +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 introduce p := first [ - match p with _ => (* Already there, generalize dependent hyps *) - generalize dependent p ; intros p - end - | intros until p | intros ]. +Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. -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 do_intros H := + (try intros until H) ; (intro_block_id H || intro_block H). -Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end. +Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; tac H. -Ltac un_dep_elimify := unfold block_dep_elim in *. +Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim. -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_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 nonrec_equations := - solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ] - || fail "Unnexpected equations goal". +(** To dependent elimination on some hyp. *) -Ltac recursive_equations := - solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ] - || fail "Unnexpected recursive equations goal". +Ltac depelim id := do_depelim ltac:(fun hyp => do_case hyp) id. -(** The [equations] tactic is the toplevel tactic for solving goals generated - by [Equations]. *) +(** Used internally. *) -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. *) +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. +Tactic Notation "dependent" "destruction" ident(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. +Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := + 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. +Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := + 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. +Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := + 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 +(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by + writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before calling [induction]. *) Tactic Notation "dependent" "induction" ident(H) := @@ -558,13 +446,8 @@ Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := (** 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. - -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. +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := + do_depelim' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H. -Ltac simplify_IH_hyps := repeat - match goal with - | [ hyp : _ |- _ ] => specialize_hypothesis hyp - end.
\ No newline at end of file +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := + do_depelim' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index a6aa4d524..89f477d8f 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -82,7 +82,7 @@ Qed. 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, propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index aff2da946..2064977fe 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -46,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 881297955..b3b08e067 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -43,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. *) @@ -105,6 +105,15 @@ 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 := @@ -121,6 +130,16 @@ 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 := |