From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 contrib/field/Field_Tactic.v | 432 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 432 insertions(+)
 create mode 100644 contrib/field/Field_Tactic.v

(limited to 'contrib/field/Field_Tactic.v')

diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
new file mode 100644
index 00000000..c5c06547
--- /dev/null
+++ b/contrib/field/Field_Tactic.v
@@ -0,0 +1,432 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: Field_Tactic.v,v 1.20.2.1 2004/07/16 19:30:09 herbelin Exp $ *)
+
+Require Import Ring.
+Require Export Field_Compl.
+Require Export Field_Theory.
+
+(**** Interpretation A --> ExprA ****)
+
+Ltac mem_assoc var lvar :=
+  match constr:lvar with
+  | (nilT _) => constr:false
+  | (consT _ ?X1 ?X2) =>
+      match constr:(X1 = var) with
+      | (?X1 = ?X1) => constr:true
+      | _ => mem_assoc var X2
+      end
+  end.
+
+Ltac seek_var_aux FT lvar trm :=
+  let AT := eval cbv beta iota delta [A] in (A FT)
+  with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
+  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
+  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
+  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
+  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
+  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  match constr:trm with
+  | AzeroT => lvar
+  | AoneT => lvar
+  | (AplusT ?X1 ?X2) =>
+      let l1 := seek_var_aux FT lvar X1 in
+      seek_var_aux FT l1 X2
+  | (AmultT ?X1 ?X2) =>
+      let l1 := seek_var_aux FT lvar X1 in
+      seek_var_aux FT l1 X2
+  | (AoppT ?X1) => seek_var_aux FT lvar X1
+  | (AinvT ?X1) => seek_var_aux FT lvar X1
+  | ?X1 =>
+      let res := mem_assoc X1 lvar in
+      match constr:res with
+      | true => lvar
+      | false => constr:(consT AT X1 lvar)
+      end
+  end.
+
+Ltac seek_var FT trm :=
+  let AT := eval cbv beta iota delta [A] in (A FT) in
+  seek_var_aux FT (nilT AT) trm.
+
+Ltac number_aux lvar cpt :=
+  match constr:lvar with
+  | (nilT ?X1) => constr:(nilT (prodT X1 nat))
+  | (consT ?X1 ?X2 ?X3) =>
+      let l2 := number_aux X3 (S cpt) in
+      constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2)
+  end.
+
+Ltac number lvar := number_aux lvar 0.
+
+Ltac build_varlist FT trm := let lvar := seek_var FT trm in
+                             number lvar.
+
+Ltac assoc elt lst :=
+  match constr:lst with
+  | (nilT _) => fail
+  | (consT (prodT _ nat) (pairT _ nat ?X1 ?X2) ?X3) =>
+      match constr:(elt = X1) with
+      | (?X1 = ?X1) => constr:X2
+      | _ => assoc elt X3
+      end
+  end.
+
+Ltac interp_A FT lvar trm :=
+  let AT := eval cbv beta iota delta [A] in (A FT)
+  with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
+  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
+  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
+  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
+  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
+  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  match constr:trm with
+  | AzeroT => constr:EAzero
+  | AoneT => constr:EAone
+  | (AplusT ?X1 ?X2) =>
+      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
+      constr:(EAplus e1 e2)
+  | (AmultT ?X1 ?X2) =>
+      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
+      constr:(EAmult e1 e2)
+  | (AoppT ?X1) =>
+      let e := interp_A FT lvar X1 in
+      constr:(EAopp e)
+  | (AinvT ?X1) => let e := interp_A FT lvar X1 in
+                   constr:(EAinv e)
+  | ?X1 => let idx := assoc X1 lvar in
+           constr:(EAvar idx)
+  end.
+
+(************************)
+(*    Simplification    *)
+(************************)
+
+(**** Generation of the multiplier ****)
+
+Ltac remove e l :=
+  match constr:l with
+  | (nilT _) => l
+  | (consT ?X1 e ?X2) => constr:X2
+  | (consT ?X1 ?X2 ?X3) => let nl := remove e X3 in
+                           constr:(consT X1 X2 nl)
+  end.
+
+Ltac union l1 l2 :=
+  match constr:l1 with
+  | (nilT _) => l2
+  | (consT ?X1 ?X2 ?X3) =>
+      let nl2 := remove X2 l2 in
+      let nl := union X3 nl2 in
+      constr:(consT X1 X2 nl)
+  end.
+
+Ltac raw_give_mult trm :=
+  match constr:trm with
+  | (EAinv ?X1) => constr:(consT ExprA X1 (nilT ExprA))
+  | (EAopp ?X1) => raw_give_mult X1
+  | (EAplus ?X1 ?X2) =>
+      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
+      union l1 l2
+  | (EAmult ?X1 ?X2) =>
+      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
+      eval compute in (appT ExprA l1 l2)
+  | _ => constr:(nilT ExprA)
+  end.
+
+Ltac give_mult trm :=
+  let ltrm := raw_give_mult trm in
+  constr:(mult_of_list ltrm).
+
+(**** Associativity ****)
+
+Ltac apply_assoc FT lvar trm :=
+  let t := eval compute in (assoc trm) in
+  match constr:(t = trm) with
+  | (?X1 = ?X1) => idtac
+  | _ =>
+      rewrite <- (assoc_correct FT trm); change (assoc trm) with t in |- *
+  end.
+
+(**** Distribution *****)
+
+Ltac apply_distrib FT lvar trm :=
+  let t := eval compute in (distrib trm) in
+  match constr:(t = trm) with
+  | (?X1 = ?X1) => idtac
+  | _ =>
+      rewrite <- (distrib_correct FT trm);
+       change (distrib trm) with t in |- *
+  end.
+
+(**** Multiplication by the inverse product ****)
+
+Ltac grep_mult := match goal with
+                  | id:(interp_ExprA _ _ _ <> _) |- _ => id
+                  end.
+
+Ltac weak_reduce :=
+  match goal with
+  |  |- context [(interp_ExprA ?X1 ?X2 _)] =>
+      cbv beta iota zeta
+       delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero
+             Aone Aplus Amult Aopp Ainv] in |- *
+  end.
+
+Ltac multiply mul :=
+  match goal with
+  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA ?X1 ?X2 ?X4) =>
+      let AzeroT := eval cbv beta iota delta [Azero X1] in (Azero X1) in
+      (cut (interp_ExprA X1 X2 mul <> AzeroT);
+        [ intro; let id := grep_mult in
+                 apply (mult_eq X1 X3 X4 mul X2 id)
+        | weak_reduce;
+           let AoneT := eval cbv beta iota delta [Aone X1] in (Aone X1)
+           with AmultT := eval cbv beta iota delta [Amult X1] in (Amult X1) in
+           (try
+             match goal with
+             |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r X1)
+             end; clear X1 X2) ])
+  end.
+
+Ltac apply_multiply FT lvar trm :=
+  let t := eval compute in (multiply trm) in
+  match constr:(t = trm) with
+  | (?X1 = ?X1) => idtac
+  | _ =>
+      rewrite <- (multiply_correct FT trm);
+       change (multiply trm) with t in |- *
+  end.
+
+(**** Permutations and simplification ****)
+
+Ltac apply_inverse mul FT lvar trm :=
+  let t := eval compute in (inverse_simplif mul trm) in
+  match constr:(t = trm) with
+  | (?X1 = ?X1) => idtac
+  | _ =>
+      rewrite <- (inverse_correct FT trm mul);
+       [ change (inverse_simplif mul trm) with t in |- * | assumption ]
+  end.
+(**** Inverse test ****)
+
+Ltac strong_fail tac := first [ tac | fail 2 ].
+
+Ltac inverse_test_aux FT trm :=
+  let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
+  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
+  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
+  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  match constr:trm with
+  | (AinvT _) => fail 1
+  | (AoppT ?X1) =>
+      strong_fail ltac:(inverse_test_aux FT X1; idtac)
+  | (AplusT ?X1 ?X2) =>
+      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
+  | (AmultT ?X1 ?X2) =>
+      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
+  | _ => idtac
+  end.
+
+Ltac inverse_test FT :=
+  let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) in
+  match goal with
+  |  |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
+  end.
+
+(**** Field itself ****)
+
+Ltac apply_simplif sfun :=
+  match goal with
+  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) => 
+  sfun X1 X2 X3
+  end;
+   match goal with
+   |  |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) => 
+   sfun X1 X2 X3
+   end.
+
+Ltac unfolds FT :=
+  match eval cbv beta iota delta [Aminus] in (Aminus FT) with
+  | (Field_Some _ ?X1) => unfold X1 in |- *
+  | _ => idtac
+  end;
+   match eval cbv beta iota delta [Adiv] in (Adiv FT) with
+   | (Field_Some _ ?X1) => unfold X1 in |- *
+   | _ => idtac
+   end.
+
+Ltac reduce FT :=
+  let AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
+  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
+  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
+  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
+  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
+  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] in |- * ||
+     compute in |- *).
+
+Ltac field_gen_aux FT :=
+  let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) in
+  match goal with
+  |  |- (?X1 = ?X2) =>
+      let lvar := build_varlist FT (AplusT X1 X2) in
+      let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in
+      let mul := give_mult (EAplus trm1 trm2) in
+      (cut
+        (let ft := FT in
+         let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
+        [ compute in |- *; auto
+        | intros ft vm; apply_simplif apply_distrib;
+           apply_simplif apply_assoc; multiply mul;
+           [ apply_simplif apply_multiply;
+              apply_simplif ltac:(apply_inverse mul);
+              let id := grep_mult in
+              clear id; weak_reduce; clear ft vm; first
+              [ inverse_test FT; ring | field_gen_aux FT ]
+           | idtac ] ])
+  end.
+
+Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
+
+(*****************************)
+(*    Term Simplification    *)
+(*****************************)
+
+(**** Minus and division expansions ****)
+
+Ltac init_exp FT trm :=
+  let e :=
+   (match eval cbv beta iota delta [Aminus] in (Aminus FT) with
+    | (Field_Some _ ?X1) => eval cbv beta delta [X1] in trm
+    | _ => trm
+    end) in
+  match eval cbv beta iota delta [Adiv] in (Adiv FT) with
+  | (Field_Some _ ?X1) => eval cbv beta delta [X1] in e
+  | _ => e
+  end.
+
+(**** Inverses simplification ****)
+
+Ltac simpl_inv trm :=
+  match constr:trm with
+  | (EAplus ?X1 ?X2) =>
+      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
+      constr:(EAplus e1 e2)
+  | (EAmult ?X1 ?X2) =>
+      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
+      constr:(EAmult e1 e2)
+  | (EAopp ?X1) => let e := simpl_inv X1 in
+                   constr:(EAopp e)
+  | (EAinv ?X1) => SimplInvAux X1
+  | ?X1 => constr:X1
+  end
+ with SimplInvAux trm :=
+  match constr:trm with
+  | (EAinv ?X1) => simpl_inv X1
+  | (EAmult ?X1 ?X2) =>
+      let e1 := simpl_inv (EAinv X1) with e2 := simpl_inv (EAinv X2) in
+      constr:(EAmult e1 e2)
+  | ?X1 => let e := simpl_inv X1 in
+           constr:(EAinv e)
+  end.
+
+(**** Monom simplification ****)
+
+Ltac map_tactic fcn lst :=
+  match constr:lst with
+  | (nilT _) => lst
+  | (consT ?X1 ?X2 ?X3) =>
+      let r := fcn X2 with t := map_tactic fcn X3 in
+      constr:(consT X1 r t)
+  end.
+
+Ltac build_monom_aux lst trm :=
+  match constr:lst with
+  | (nilT _) => eval compute in (assoc trm)
+  | (consT _ ?X1 ?X2) => build_monom_aux X2 (EAmult trm X1)
+  end.
+
+Ltac build_monom lnum lden :=
+  let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in
+  let ltot := eval compute in (appT ExprA lnum ildn) in
+  let trm := build_monom_aux ltot EAone in
+  match constr:trm with
+  | (EAmult _ ?X1) => constr:X1
+  | ?X1 => constr:X1
+  end.
+
+Ltac simpl_monom_aux lnum lden trm :=
+  match constr:trm with
+  | (EAmult (EAinv ?X1) ?X2) =>
+      let mma := mem_assoc X1 lnum in
+      match constr:mma with
+      | true =>
+          let newlnum := remove X1 lnum in
+          simpl_monom_aux newlnum lden X2
+      | false => simpl_monom_aux lnum (consT ExprA X1 lden) X2
+      end
+  | (EAmult ?X1 ?X2) =>
+      let mma := mem_assoc X1 lden in
+      match constr:mma with
+      | true =>
+          let newlden := remove X1 lden in
+          simpl_monom_aux lnum newlden X2
+      | false => simpl_monom_aux (consT ExprA X1 lnum) lden X2
+      end
+  | (EAinv ?X1) =>
+      let mma := mem_assoc X1 lnum in
+      match constr:mma with
+      | true =>
+          let newlnum := remove X1 lnum in
+          build_monom newlnum lden
+      | false => build_monom lnum (consT ExprA X1 lden)
+      end
+  | ?X1 =>
+      let mma := mem_assoc X1 lden in
+      match constr:mma with
+      | true =>
+          let newlden := remove X1 lden in
+          build_monom lnum newlden
+      | false => build_monom (consT ExprA X1 lnum) lden
+      end
+  end.
+
+Ltac simpl_monom trm := simpl_monom_aux (nilT ExprA) (nilT ExprA) trm.
+
+Ltac simpl_all_monomials trm :=
+  match constr:trm with
+  | (EAplus ?X1 ?X2) =>
+      let e1 := simpl_monom X1 with e2 := simpl_all_monomials X2 in
+      constr:(EAplus e1 e2)
+  | ?X1 => simpl_monom X1
+  end.
+
+(**** Associativity and distribution ****)
+
+Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)).
+
+(**** The tactic Field_Term ****)
+
+Ltac eval_weak_reduce trm :=
+  eval
+   cbv beta iota zeta
+    delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus
+          Amult Aopp Ainv] in trm.
+
+Ltac field_term FT exp :=
+  let newexp := init_exp FT exp in
+  let lvar := build_varlist FT newexp in
+  let trm := interp_A FT lvar newexp in
+  let tma := eval compute in (assoc trm) in
+  let tsmp :=
+   simpl_all_monomials
+    ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
+  let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
+  (replace exp with trep; [ ring trep | field_gen FT ]).
\ No newline at end of file
-- 
cgit v1.2.3