diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 26 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 11 |
2 files changed, 28 insertions, 9 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 53e12723..b9eb8f80 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 13492 2010-10-04 21:20:01Z herbelin $ i*) +(*i $Id: Equality.v 13730 2010-12-19 13:32:01Z msozeau $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -320,19 +320,35 @@ Hint Unfold solution_left solution_right deletion simplification_heq constructor forms). Compare with the lemma 16 of the paper. We don't have a [noCycle] procedure yet. *) +Ltac block_equality id := + match type of id with + | @eq ?A ?t ?u => change (block (@eq A t u)) in id + | _ => idtac + end. + +Ltac revert_blocking_until id := + Tactics.on_last_hyp ltac:(fun id' => + match id' with + | id => idtac + | _ => block_equality id' ; revert id' ; revert_blocking_until id + end). + 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 _ ?p _) (existT _ ?q _) -> _ => refine (simplification_existT2 _ _ _ _ _ _ _) || - refine (simplification_existT1 _ _ _ _ _ _ _ _) + match goal with + | H : p = q |- _ => intro + | _ => refine (simplification_existT1 _ _ _ _ _ _ _ _) + end | ?x = ?y -> _ => (* variables case *) (let hyp := fresh in intros hyp ; - move hyp before x ; revert_until hyp ; generalize dependent x ; + move hyp before x ; revert_blocking_until hyp ; generalize dependent x ; refine (solution_left _ _ _ _)(* ; intros until 0 *)) || (let hyp := fresh in intros hyp ; - move hyp before y ; revert_until hyp ; generalize dependent y ; + move hyp before y ; revert_blocking_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 diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 333dd7a6..4a41d9c9 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: Tactics.v 13693 2010-12-08 15:32:25Z msozeau $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) @@ -308,11 +308,14 @@ Ltac program_simplify := subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). -Ltac program_solve_wf := +(** We only try to solve proposition goals automatically. *) + +Ltac program_solve := match goal with - |- well_founded _ => auto with * + | |- well_founded _ => auto with * + | |- ?T => match type of T with Prop => auto end end. -Ltac program_simpl := program_simplify ; auto; try program_solve_wf. +Ltac program_simpl := program_simplify ; try program_solve. Obligation Tactic := program_simpl. |