diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-07 00:10:42 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-07 00:10:42 +0000 |
commit | a5e035d42a7043bcafe392c8e964ce85558cd319 (patch) | |
tree | a95c9cb9907616efe8851a934f59c7b413d011c7 /theories/Program | |
parent | 0e189432da864d7e31c9d6bb2355f349308a3d0a (diff) |
More debugging of [Equations], now able to discharge even the heavily
dependent [noConfusion] definitions in "A Few Constructions on
Constructors". Now the guardness check is blocking.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11374 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Equality.v | 170 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 35 |
2 files changed, 168 insertions, 37 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index d11996a67..3e0e8ca2b 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Program.Equality"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -19,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 := @@ -309,17 +314,15 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) " 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. - -*) + Goguen, McBride and McKinna. *) (** 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; assumption. Defined. +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; assumption. Defined. +Proof. intros; subst; apply X. Defined. Lemma deletion : Π A B (t : A), B -> (t = t -> B). Proof. intros; assumption. Defined. @@ -331,6 +334,21 @@ Lemma simplification_existT : Π 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_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. + +(** 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. + (** This hint database and the following tactic can be used with [autosimpl] to unfold everything to [eq_rect]s. *) @@ -354,18 +372,20 @@ Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs). Ltac simplify_one_dep_elim_term c := match c with | @JMeq ?A ?a ?A ?b -> _ => refine (simplification_heq _ _ _ _ _) - | ?t = ?t -> _ => intros _ + | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _) | eq (existT ?P ?p _) (existT ?P ?p _) -> _ => refine (simplification_existT _ _ _ _ _ _ _) - | ?f ?x = ?f ?y -> _ => let H := fresh in intros H ; injection H ; clear H | ?x = ?y -> _ => - (let hyp := fresh in intros hyp ; - move dependent hyp before x ; + (let hyp := fresh in intros hyp ; + move dependent hyp before x ; generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) || - (let hyp := fresh in intros hyp ; - move dependent hyp before y ; + (let hyp := fresh in intros hyp ; + move dependent 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 intros H ; injection H ; clear H | ?t = ?u -> _ => let hyp := fresh in intros hyp ; elimtype False ; discriminate + | id ?T => fail 1 (* Do not put any part of the rhs in the hyps *) | _ => intro end. @@ -392,32 +412,59 @@ Ltac destruct_last := (** 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. *) -Ltac try_intros m := - (eapply m ; eauto) || (intro ; try_intros m). +Ltac simpl_apply m := refine m. (* || apply m || simpl ; apply m. *) + +Ltac try_intros m := unfold Datatypes.id ; refine m || apply m. (* (repeat simpl_apply m || intro). *) (** 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 H := clear H ; simplify_dep_elim ; reverse. +Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local. -(** Solving a method call: we must refine the goal until the body - can be applied or just solve it by splitting on an empty family member. *) +(** 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 |- _ ] => simplify_method H ; solve_empty body - | [ H := ?body |- _ ] => simplify_method H ; rec ; try_intros body + | [ H := ?body : nat |- _ ] => subst H ; clear ; abstract (simplify_method idtac ; solve_empty body) + | [ H := ?body |- _ ] => clear H ; simplify_method ltac:(exact body) ; rec ; try_intros body end. (** Impossible cases, by splitting on a given target. *) Ltac solve_split := match goal with - | [ |- let split := ?x : nat in _ ] => intros _ ; solve_empty x + | [ |- let split := ?x : nat in _ ] => clear ; abstract (intros _ ; solve_empty x) end. (** If defining recursive functions, the prototypes come first. *) @@ -428,19 +475,98 @@ Ltac intro_prototypes := | _ => idtac end. +Ltac case_last := + match goal with + | [ p : ?x = ?x |- ?T ] => change (id T) ; revert p ; refine (simplification_K _ x _ _) + | [ p : ?x = ?y |- ?T ] => change (id T) ; revert p + | [ p : _ |- ?T ] => simpl in p ; change (id T) ; generalize_eqs p ; destruct p + end. + Ltac nonrec_equations := - solve [solve_equations (solve_method idtac)] || solve [ solve_split ] + solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ] || fail "Unnexpected equations goal". Ltac recursive_equations := - solve [solve_equations (solve_method ltac:intro)] || solve [ solve_split ] + 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 := +Ltac equations := set_eos ; match goal with | [ |- Π x : _, _ ] => intro ; recursive_equations | _ => nonrec_equations end. + +Equations NoConfusion_nat (P : Prop) (x y : nat) : Prop := +NoConfusion_nat P 0 0 := P -> P ; +NoConfusion_nat P 0 (S y) := P ; +NoConfusion_nat P (S x) 0 := P ; +NoConfusion_nat P (S x) (S y) := (x = y -> P) -> P. +Debug Off. + Solve Obligations using equations. + +Equations noConfusion_nat (P : Prop) (x y : nat) (H : x = y) : NoConfusion_nat P x y := +noConfusion_nat P 0 0 refl := λ p, p ; +noConfusion_nat P (S n) (S n) refl := λ p : n = n -> P, p refl. + + Solve Obligations using equations. + +Instance nat_noconf : NoConfusionPackage nat := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_nat P x y ; + noConfusion := λ P x y, noConfusion_nat P x y. + +Equations NoConfusion_bool (P : Prop) (x y : bool) : Prop := +NoConfusion_bool P true true := P -> P ; +NoConfusion_bool P false false := P -> P ; +NoConfusion_bool P true false := P ; +NoConfusion_bool P false true := P. + + Solve Obligations using equations. + +Equations noConfusion_bool (P : Prop) (x y : bool) (H : x = y) : NoConfusion_bool P x y := +noConfusion_bool P true true refl := λ p, p ; +noConfusion_bool P false false refl := λ p, p. + + Solve Obligations using equations. + +Instance bool_noconf : NoConfusionPackage bool := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_bool P x y ; + noConfusion := λ P x y, noConfusion_bool P x y. + +Equations NoConfusion_unit (P : Prop) (x y : unit) : Prop := +NoConfusion_unit P tt tt := P -> P. + + Solve Obligations using equations. + +Equations noConfusion_unit (P : Prop) (x y : unit) (H : x = y) : NoConfusion_unit P x y := +noConfusion_unit P tt tt refl := λ p, p. + + Solve Obligations using equations. + +Instance unit_noconf : NoConfusionPackage unit := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_unit P x y ; + noConfusion := λ P x y, noConfusion_unit P x y. + +Require Import List. + +Implicit Arguments nil [[A]]. + +Equations NoConfusion_list (P : Prop) (A : Type) (x y : list A) : Prop := +NoConfusion_list P A nil nil := P -> P ; +NoConfusion_list P A nil (cons a y) := P ; +NoConfusion_list P A (cons a x) nil := P ; +NoConfusion_list P A (cons a x) (cons b y) := (a = b -> x = y -> P) -> P. + + Solve Obligations using equations. + +Equations noConfusion_list (P : Prop) A (x y : list A) (H : x = y) : NoConfusion_list P A x y := +noConfusion_list P A nil nil refl := λ p, p ; +noConfusion_list P A (cons a x) (cons a x) refl := λ p : a = a -> x = x -> P, p refl refl. + + Solve Obligations using equations. + +Instance list_noconf A : NoConfusionPackage (list A) := + NoConfusion := λ P, Π x y, x = y -> NoConfusion_list P A x y ; + noConfusion := λ P x y, noConfusion_list P A x y. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 7fe5211af..9cb7725c0 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -121,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. *) @@ -213,21 +233,6 @@ Ltac replace_hyp H c := let H' := fresh "H" in assert(H' := c) ; clear H ; rename H' into H. -(** A tactic to refine an hypothesis by supplying some of its arguments. *) - -Ltac refine_hyp c := - let tac H := replace_hyp H c in - match c with - | ?H _ => tac H - | ?H _ _ => tac H - | ?H _ _ _ => tac H - | ?H _ _ _ _ => tac H - | ?H _ _ _ _ _ => tac H - | ?H _ _ _ _ _ _ => tac H - | ?H _ _ _ _ _ _ _ => tac H - | ?H _ _ _ _ _ _ _ _ => tac H - 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, possibly using [program_simplify] to use standard goal-cleaning tactics. *) |