From 9c2662eecc398f38be3b6280a8f760cc439bc31c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 21 Jan 2016 01:43:10 +0100 Subject: Stronger invariants on the use of the introduction pattern (pat1,...,patn). The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these. --- theories/Wellfounded/Lexicographic_Exponentiation.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Wellfounded') diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index b8b9e929c..e05dab7a4 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -75,7 +75,7 @@ Section Wf_Lexicographic_Exponentiation. Proof. intros. inversion H. - - apply app_cons_not_nil in H1 as (). + - apply app_cons_not_nil in H1 as []. - assert (x ++ [a] = [x0]) by auto with sets. apply app_eq_unit in H0 as [(->, _)| (_, [=])]. auto using d_nil. @@ -98,7 +98,7 @@ Section Wf_Lexicographic_Exponentiation. destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)%app_inj_tail, <-). inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ]. - inversion H0. - + apply app_cons_not_nil in H3 as (). + + apply app_cons_not_nil in H3 as []. + rewrite app_comm_cons in H0, H1. apply desc_prefix in H0. pose proof (H x0 b H0). apply rt_trans with (y := x0); auto with sets. @@ -145,7 +145,7 @@ Section Wf_Lexicographic_Exponentiation. pose proof H0 as H0'. apply app_inj_tail in H0' as (_, ->). rewrite app_assoc_reverse in H0. - apply Hind in H0 as (). + apply Hind in H0 as []. split. assumption. apply d_conc; auto with sets. -- cgit v1.2.3