diff options
author | 2001-06-27 14:13:15 +0000 | |
---|---|---|
committer | 2001-06-27 14:13:15 +0000 | |
commit | bf86a8e1a180d60d5a065b5af5ff14b5286a2015 (patch) | |
tree | 815b401aad63db0864b438714091f82551b699b9 | |
parent | 034c8ee48c27cdb4be3671403009d2f9c3238662 (diff) |
Reduction tres significative du terme preuve
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1811 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/field/Field_Tactic.v | 24 | ||||
-rw-r--r-- | contrib/field/Field_Theory.v | 4 |
2 files changed, 16 insertions, 12 deletions
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v index 4b676e8bb..9a1a1b057 100644 --- a/contrib/field/Field_Tactic.v +++ b/contrib/field/Field_Tactic.v @@ -147,8 +147,9 @@ Tactic Definition ApplyAssoc FT lvar trm := Cut (interp_ExprA FT lvar (assoc trm))==(interp_ExprA FT lvar trm); [Intro; (Match Context With - | [id:(interp_ExprA ? ? (assoc ?))== ? |- ?] -> - Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota) + | [id:(interp_ExprA ?1 ?2 (assoc ?3))== ?4 |- ?] -> + Let t=Eval Compute in (assoc ?3) In + Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id) |Apply assoc_correct]. (**** Distribution *****) @@ -157,8 +158,9 @@ Tactic Definition ApplyDistrib FT lvar trm := Cut (interp_ExprA FT lvar (distrib trm))==(interp_ExprA FT lvar trm); [Intro; (Match Context With - | [id:(interp_ExprA ? ? (distrib ?))== ? |- ?] -> - Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota) + | [id:(interp_ExprA ?1 ?2 (distrib ?3))== ?4 |- ?] -> + Let t=Eval Compute in (distrib ?3) In + Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id) |Apply distrib_correct]. (**** Multiplication by the inverse product ****) @@ -174,8 +176,8 @@ Tactic Definition Multiply mul := Cut ~(interp_ExprA ?1 ?2 mul)==AzeroT; [Intro; Let id = GrepMult In - Apply (mult_eq ?1 ?3 ?4 mul ?2 id); - Cbv Beta Delta -[interp_ExprA] Iota + Apply (mult_eq ?1 ?3 ?4 mul ?2 id)(*; + Cbv Beta Delta -[interp_ExprA] Iota*) |Cbv Beta Delta -[not] Iota; Let AmultT = Eval Compute in (Amult ?1) And AoneT = Eval Compute in (Aone ?1) In @@ -186,8 +188,9 @@ Tactic Definition ApplyMultiply FT lvar trm := Cut (interp_ExprA FT lvar (multiply trm))==(interp_ExprA FT lvar trm); [Intro; (Match Context With - | [id:(interp_ExprA ? ? (multiply ?))== ? |- ?] -> - Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota) + | [id:(interp_ExprA ?1 ?2 (multiply ?3))== ?4 |- ?] -> + Let t=Eval Compute in (multiply ?3) In + Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id) |Apply multiply_correct]. (**** Permutations and simplification ****) @@ -197,8 +200,9 @@ Tactic Definition ApplyInverse mul FT lvar trm := (interp_ExprA FT lvar trm); [Intro; (Match Context With - | [id:(interp_ExprA ? ? (inverse_simplif ? ?))== ? |- ?] -> - Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota) + | [id:(interp_ExprA ?1 ?2 (inverse_simplif ?3 ?4))== ?5 |- ?] -> + Let t=Eval Compute in (inverse_simplif ?3 ?4) In + Change (interp_ExprA ?1 ?2 t)== ?5 in id;Try (Rewrite <- id);Clear id) |Apply inverse_correct;Assumption]. (**** Inverse test ****) diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v index 2cd2f09a6..5cdd5eacd 100644 --- a/contrib/field/Field_Theory.v +++ b/contrib/field/Field_Theory.v @@ -194,8 +194,8 @@ Save. Fixpoint interp_ExprA [lvar:(list (Sprod AT nat));e:ExprA] : AT := Cases e of - | EAzero => AzeroT - | EAone => AoneT + | EAzero => AzeroT + | EAone => AoneT | (EAplus e1 e2) => (AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2)) | (EAmult e1 e2) => (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)) | (EAopp e) => ((Aopp T) (interp_ExprA lvar e)) |