|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Ring_tac BinList Ring_polynom InitialRing.
Require Export Field_theory.
(* syntaxification *)
(* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
(* the tactic could be used to discriminate occurrences of an opaque *)
(* constant phi, with (phi 0) not convertible to 0 for instance *)
Ltac mkFieldexpr C Cst CstPow rO rI radd rmul rsub ropp rdiv rinv rpow t fv :=
let rec mkP t :=
let f :=
match Cst t with
| InitialRing.NotConstant =>
match t with
| rO =>
fun _ => constr:(@FEO C)
| rI =>
fun _ => constr:(@FEI C)
| (radd ?t1 ?t2) =>
fun _ =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(@FEadd C e1 e2)
| (rmul ?t1 ?t2) =>
fun _ =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(@FEmul C e1 e2)
| (rsub ?t1 ?t2) =>
fun _ =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(@FEsub C e1 e2)
| (ropp ?t1) =>
fun _ => let e1 := mkP t1 in constr:(@FEopp C e1)
| (rdiv ?t1 ?t2) =>
fun _ =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(@FEdiv C e1 e2)
| (rinv ?t1) =>
fun _ => let e1 := mkP t1 in constr:(@FEinv C e1)
| (rpow ?t1 ?n) =>
match CstPow n with
| InitialRing.NotConstant =>
fun _ =>
let p := Find_at t fv in
constr:(@FEX C p)
| ?c => fun _ => let e1 := mkP t1 in constr:(@FEpow C e1 c)
end
| _ =>
fun _ =>
let p := Find_at t fv in
constr:(@FEX C p)
end
| ?c => fun _ => constr:(@FEc C c)
end in
f ()
in mkP t.
(* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
(* the tactic could be used to discriminate occurrences of an opaque *)
(* constant phi, with (phi 0) not convertible to 0 for instance *)
Ltac FFV Cst CstPow rO rI add mul sub opp div inv pow t fv :=
let rec TFV t fv :=
match Cst t with
| InitialRing.NotConstant =>
match t with
| rO => fv
| rI => fv
| (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (opp ?t1) => TFV t1 fv
| (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (inv ?t1) => TFV t1 fv
| (pow ?t1 ?n) =>
match CstPow n with
| InitialRing.NotConstant =>
AddFvTail t fv
| _ => TFV t1 fv
end
| _ => AddFvTail t fv
end
| _ => fv
end
in TFV t fv.
(* packaging the field structure *)
(* TODO: inline PackField into field_lookup *)
Ltac PackField F req Cst_tac Pow_tac L1 L2 L3 L4 cond_ok pre post :=
let FLD :=
match type of L1 with
| context [req (@FEeval ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
(fun proj =>
proj Cst_tac Pow_tac pre post
req rO rI radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
| _ => fail 1 "field anomaly: bad correctness lemma (parse)"
end in
F FLD.
Ltac get_FldPre FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
pre).
Ltac get_FldPost FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
post).
Ltac get_L1 FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
L1).
Ltac get_SimplifyEqLemma FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
L2).
Ltac get_SimplifyLemma FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
L3).
Ltac get_L4 FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
L4).
Ltac get_CondLemma FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
cond_ok).
Ltac get_FldEq FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
req).
Ltac get_FldCarrier FLD :=
let req := get_FldEq FLD in
relation_carrier req.
Ltac get_RingFV FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
FV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow).
Ltac get_FFV FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
FFV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow).
Ltac get_RingMeta FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow).
Ltac get_Meta FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
mkFieldexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow).
Ltac get_Hyp_tac FLD :=
FLD ltac:
(fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
let mkPol := mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow in
fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
Ltac get_FEeval FLD :=
let L1 := get_L1 FLD in
match type of L1 with
| context
[(@FEeval
?R ?r0 ?r1 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
constr:(@FEeval R r0 r1 add mul sub opp div inv C phi Cpow powphi pow)
| _ => fail 1 "field anomaly: bad correctness lemma (get_FEeval)"
end.
(* simplifying the non-zero condition... *)
Ltac fold_field_cond req :=
let rec fold_concl t :=
match t with
?x /\ ?y =>
let fx := fold_concl x in let fy := fold_concl y in constr:(fx/\fy)
| req ?x ?y -> False => constr:(~ req x y)
| _ => t
end in
let ft := fold_concl Get_goal in
change ft.
Ltac simpl_PCond FLD :=
let req := get_FldEq FLD in
let lemma := get_CondLemma FLD in
try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
protect_fv "field_cond";
fold_field_cond req;
try exact I.
Ltac simpl_PCond_BEURK FLD :=
let req := get_FldEq FLD in
let lemma := get_CondLemma FLD in
(apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
protect_fv "field_cond";
fold_field_cond req.
(* Rewriting (field_simplify) *)
Ltac Field_norm_gen f n FLD lH rl :=
let mkFV := get_RingFV FLD in
let mkFFV := get_FFV FLD in
let mkFE := get_Meta FLD in
let fv0 := FV_hypo_tac mkFV ltac:(get_FldEq FLD) lH in
let lemma_tac fv kont :=
let lemma := get_SimplifyLemma FLD in
(* reify equations of the context *)
let lpe := get_Hyp_tac FLD fv lH in
let vlpe := fresh "hyps" in
pose (vlpe := lpe);
let prh := proofHyp_tac lH in
(* compute the normal form of the reified hyps *)
let vlmp := fresh "hyps'" in
let vlmp_eq := fresh "hyps_eq" in
let mk_monpol := get_MonPol lemma in
compute_assertion vlmp_eq vlmp (mk_monpol vlpe);
(* partially instantiate the lemma *)
let lem := fresh "f_rw_lemma" in
(assert (lem := lemma n vlpe fv prh vlmp vlmp_eq)
|| fail "type error when building the rewriting lemma");
(* continuation will call main_tac for all reified terms *)
kont lem;
(* at the end, cleanup *)
(clear lem vlmp_eq vlmp vlpe||idtac"Field_norm_gen:cleanup failed") in
(* each instance of the lemma is simplified then passed to f *)
let main_tac H := protect_fv "field" in H; f H in
(* generate and use equations for each expression *)
ReflexiveRewriteTactic mkFFV mkFE lemma_tac main_tac fv0 rl;
try simpl_PCond FLD.
Ltac Field_simplify_gen f FLD lH rl :=
get_FldPre FLD ();
Field_norm_gen f ring_subst_niter FLD lH rl;
get_FldPost FLD ().
Ltac Field_simplify :=
Field_simplify_gen ltac:(fun H => rewrite H).
Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
let G := Get_goal in
field_lookup (PackField Field_simplify) [] rl G.
Tactic Notation (at level 0)
"field_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
let G := Get_goal in
field_lookup (PackField Field_simplify) [lH] rl G.
Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=
let G := Get_goal in
let t := type of H in
let g := fresh "goal" in
set (g:= G);
revert H;
field_lookup (PackField Field_simplify) [] rl t;
intro H;
unfold g;clear g.
Tactic Notation "field_simplify"
"["constr_list(lH) "]" constr_list(rl) "in" hyp(H):=
let G := Get_goal in
let t := type of H in
let g := fresh "goal" in
set (g:= G);
revert H;
field_lookup (PackField Field_simplify) [lH] rl t;
intro H;
unfold g;clear g.
(*
Ltac Field_simplify_in hyp:=
Field_simplify_gen ltac:(fun H => rewrite H in hyp).
Tactic Notation (at level 0)
"field_simplify" constr_list(rl) "in" hyp(h) :=
let t := type of h in
field_lookup (Field_simplify_in h) [] rl t.
Tactic Notation (at level 0)
"field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) :=
let t := type of h in
field_lookup (Field_simplify_in h) [lH] rl t.
*)
(** Generic tactic for solving equations *)
Ltac Field_Scheme Simpl_tac n lemma FLD lH :=
let req := get_FldEq FLD in
let mkFV := get_RingFV FLD in
let mkFFV := get_FFV FLD in
let mkFE := get_Meta FLD in
let Main_eq t1 t2 :=
let fv := FV_hypo_tac mkFV req lH in
let fv := mkFFV t1 fv in
let fv := mkFFV t2 fv in
let lpe := get_Hyp_tac FLD fv lH in
let prh := proofHyp_tac lH in
let vlpe := fresh "list_hyp" in
let fe1 := mkFE t1 fv in
let fe2 := mkFE t2 fv in
pose (vlpe := lpe);
let nlemma := fresh "field_lemma" in
(assert (nlemma := lemma n fv vlpe fe1 fe2 prh)
|| fail "field anomaly:failed to build lemma");
ProveLemmaHyps nlemma
ltac:(fun ilemma =>
apply ilemma
|| fail "field anomaly: failed in applying lemma";
[ Simpl_tac | simpl_PCond FLD]);
clear nlemma;
subst vlpe in
OnEquation req Main_eq.
(* solve completely a field equation, leaving non-zero conditions to be
proved (field) *)
Ltac FIELD FLD lH rl :=
let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in
let lemma := get_L1 FLD in
get_FldPre FLD ();
Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
try exact I;
get_FldPost FLD().
Tactic Notation (at level 0) "field" :=
let G := Get_goal in
field_lookup (PackField FIELD) [] G.
Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" :=
let G := Get_goal in
field_lookup (PackField FIELD) [lH] G.
(* transforms a field equation to an equivalent (simplified) ring equation,
and leaves non-zero conditions to be proved (field_simplify_eq) *)
Ltac FIELD_SIMPL FLD lH rl :=
let Simpl := (protect_fv "field") in
let lemma := get_SimplifyEqLemma FLD in
get_FldPre FLD ();
Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
get_FldPost FLD ().
Tactic Notation (at level 0) "field_simplify_eq" :=
let G := Get_goal in
field_lookup (PackField FIELD_SIMPL) [] G.
Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=
let G := Get_goal in
field_lookup (PackField FIELD_SIMPL) [lH] G.
(* Same as FIELD_SIMPL but in hypothesis *)
Ltac Field_simplify_eq n FLD lH :=
let req := get_FldEq FLD in
let mkFV := get_RingFV FLD in
let mkFFV := get_FFV FLD in
let mkFE := get_Meta FLD in
let lemma := get_L4 FLD in
let hyp := fresh "hyp" in
intro hyp;
OnEquationHyp req hyp ltac:(fun t1 t2 =>
let fv := FV_hypo_tac mkFV req lH in
let fv := mkFFV t1 fv in
let fv := mkFFV t2 fv in
let lpe := get_Hyp_tac FLD fv lH in
let prh := proofHyp_tac lH in
let fe1 := mkFE t1 fv in
let fe2 := mkFE t2 fv in
let vlpe := fresh "vlpe" in
ProveLemmaHyps (lemma n fv lpe fe1 fe2 prh)
ltac:(fun ilemma =>
match type of ilemma with
| req _ _ -> _ -> ?EQ =>
let tmp := fresh "tmp" in
assert (tmp : EQ);
[ apply ilemma; [ exact hyp | simpl_PCond_BEURK FLD]
| protect_fv "field" in tmp; revert tmp ];
clear hyp
end)).
Ltac FIELD_SIMPL_EQ FLD lH rl :=
get_FldPre FLD ();
Field_simplify_eq Ring_tac.ring_subst_niter FLD lH;
get_FldPost FLD ().
Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) :=
let t := type of H in
generalize H;
field_lookup (PackField FIELD_SIMPL_EQ) [] t;
[ try exact I
| clear H;intro H].
Tactic Notation (at level 0)
"field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) :=
let t := type of H in
generalize H;
field_lookup (PackField FIELD_SIMPL_EQ) [lH] t;
[ try exact I
|clear H;intro H].
(* More generic tactics to build variants of field *)
(* This tactic reifies c and pass to F:
- the FLD structure gathering all info in the field DB
- the atom list
- the expression (FExpr)
*)
Ltac gen_with_field F c :=
let MetaExpr FLD _ rl :=
let R := get_FldCarrier FLD in
let mkFFV := get_FFV FLD in
let mkFE := get_Meta FLD in
let csr :=
match rl with
| List.cons ?r _ => r
| _ => fail 1 "anomaly: ill-formed list"
end in
let fv := mkFFV csr (@List.nil R) in
let expr := mkFE csr fv in
F FLD fv expr in
field_lookup (PackField MetaExpr) [] (c=c).
(* pushes the equation expr = ope(expr) in the goal, and
discharge it with field *)
Ltac prove_field_eqn ope FLD fv expr :=
let res := ope expr in
let expr' := fresh "input_expr" in
pose (expr' := expr);
let res' := fresh "result" in
pose (res' := res);
let lemma := get_L1 FLD in
let lemma :=
constr:(lemma O fv List.nil expr' res' I List.nil (eq_refl _)) in
let ty := type of lemma in
let lhs := match ty with
forall _, ?lhs=_ -> _ => lhs
end in
let rhs := match ty with
forall _, _=_ -> forall _, ?rhs=_ -> _ => rhs
end in
let lhs' := fresh "lhs" in let lhs_eq := fresh "lhs_eq" in
let rhs' := fresh "rhs" in let rhs_eq := fresh "rhs_eq" in
compute_assertion lhs_eq lhs' lhs;
compute_assertion rhs_eq rhs' rhs;
let H := fresh "fld_eqn" in
refine (_ (lemma lhs' lhs_eq rhs' rhs_eq _ _));
(* main goal *)
[intro H;protect_fv "field" in H; revert H
(* ring-nf(lhs') = ring-nf(rhs') *)
| vm_compute; reflexivity || fail "field cannot prove this equality"
(* denominator condition *)
| simpl_PCond FLD];
clear lhs_eq rhs_eq; subst lhs' rhs'.
Ltac prove_with_field ope c :=
gen_with_field ltac:(prove_field_eqn ope) c.
(* Prove an equation x=ope(x) and rewrite with it *)
Ltac prove_rw ope x :=
prove_with_field ope x;
[ let H := fresh "Heq_maple" in
intro H; rewrite H; clear H
|..].
(* Apply ope (FExpr->FExpr) on an expression *)
Ltac reduce_field_expr ope kont FLD fv expr :=
let evfun := get_FEeval FLD in
let res := ope expr in
let c := (eval simpl_field_expr in (evfun fv res)) in
kont c.
(* Hack to let a Ltac return a term in the context of a primitive tactic *)
Ltac return_term x := generalize (eq_refl x).
Ltac get_term :=
match goal with
| |- ?x = _ -> _ => x
end.
(* Turn an operation on field expressions (FExpr) into a reduction
on terms (in the field carrier). Because of field_lookup,
the tactic cannot return a term directly, so it is returned
via the conclusion of the goal (return_term). *)
Ltac reduce_field_ope ope c :=
gen_with_field ltac:(reduce_field_expr ope return_term) c.
(* Adding a new field *)
Ltac ring_of_field f :=
match type of f with
| almost_field_theory _ _ _ _ _ _ _ _ _ => constr:(AF_AR f)
| field_theory _ _ _ _ _ _ _ _ _ => constr:(F_R f)
| semi_field_theory _ _ _ _ _ _ _ => constr:(SF_SR f)
end.
Ltac coerce_to_almost_field set ext f :=
match type of f with
| almost_field_theory _ _ _ _ _ _ _ _ _ => f
| field_theory _ _ _ _ _ _ _ _ _ => constr:(F2AF set ext f)
| semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f)
end.
Ltac field_elements set ext fspec pspec sspec dspec rk :=
let afth := coerce_to_almost_field set ext fspec in
let rspec := ring_of_field fspec in
ring_elements set ext rspec pspec sspec dspec rk
ltac:(fun arth ext_r morph p_spec s_spec d_spec f => f afth ext_r morph p_spec s_spec d_spec).
Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
let get_lemma :=
match pspec with None => fun x y => x | _ => fun x y => y end in
let simpl_eq_lemma := get_lemma
Field_simplify_eq_correct Field_simplify_eq_pow_correct in
let simpl_eq_in_lemma := get_lemma
Field_simplify_eq_in_correct Field_simplify_eq_pow_in_correct in
let rw_lemma := get_lemma
Field_rw_correct Field_rw_pow_correct in
field_elements set ext fspec pspec sspec dspec rk
ltac:(fun afth ext_r morph p_spec s_spec d_spec =>
match morph with
| _ =>
let field_ok1 := constr:(Field_correct set ext_r inv_m afth morph) in
match p_spec with
| mkhypo ?pp_spec =>
let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in
match s_spec with
| mkhypo ?ss_spec =>
match d_spec with
| mkhypo ?dd_spec =>
let field_ok := constr:(field_ok2 _ dd_spec) in
let mk_lemma lemma :=
constr:(lemma _ _ _ _ _ _ _ _ _ _
set ext_r inv_m afth
_ _ _ _ _ _ _ _ _ morph
_ _ _ pp_spec _ ss_spec _ dd_spec) in
let field_simpl_eq_ok := mk_lemma simpl_eq_lemma in
let field_simpl_ok := mk_lemma rw_lemma in
let field_simpl_eq_in := mk_lemma simpl_eq_in_lemma in
let cond1_ok :=
constr:(Pcond_simpl_gen set ext_r afth morph pp_spec dd_spec) in
let cond2_ok :=
constr:(Pcond_simpl_complete set ext_r afth morph pp_spec dd_spec) in
(fun f =>
f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
cond1_ok cond2_ok)
| _ => fail 4 "field: bad coefficient division specification"
end
| _ => fail 3 "field: bad sign specification"
end
| _ => fail 2 "field: bad power specification"
end
| _ => fail 1 "field internal error : field_lemmas, please report"
end).
¤ Dauer der Verarbeitung: 0.30 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
