diff options
Diffstat (limited to 'contrib/setoid_ring/Field_tac.v')
| -rw-r--r-- | contrib/setoid_ring/Field_tac.v | 185 |
1 files changed, 93 insertions, 92 deletions
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index aad3a580..cccee604 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -67,12 +67,12 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := end in TFV t fv. -Ltac ParseFieldComponents lemma := +Ltac ParseFieldComponents lemma req := match type of lemma with | context [ (* PCond _ _ _ _ _ _ _ _ _ _ _ -> *) - (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv - ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) ] => + req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv + ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] => (fun f => f radd rmul rsub ropp rdiv rinv rpow C) | _ => fail 1 "field anomaly: bad correctness lemma (parse)" end. @@ -119,18 +119,18 @@ Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl := let prh := proofHyp_tac lH in pose (vlpe := lpe); match type of lemma with - | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] => + | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _] => compute_assertion vlmp_eq vlmp - (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe); + (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe); (assert (rr_lemma := lemma n vlpe fv prh vlmp vlmp_eq) - || fail "type error when build the rewriting lemma"); + || fail 1 "type error when build the rewriting lemma"); RW_tac rr_lemma; try clear rr_lemma vlmp_eq vlmp vlpe | _ => fail 1 "field_simplify anomaly: bad correctness lemma" end in ReflexiveRewriteTactic mkFFV mkFE simpl_field lemma_tac fv rl; try (apply Cond_lemma; simpl_PCond req) in - ParseFieldComponents lemma Main. + ParseFieldComponents lemma req Main. Ltac Field_simplify_gen f := fun req cst_tac pow_tac _ _ field_simplify_ok _ cond_ok pre post lH rl => @@ -141,33 +141,35 @@ Ltac Field_simplify_gen f := Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H). -Tactic Notation (at level 0) - "field_simplify" constr_list(rl) := - match goal with [|- ?G] => field_lookup Field_simplify [] rl [G] end. +Tactic Notation (at level 0) "field_simplify" constr_list(rl) := + let G := Get_goal in + field_lookup Field_simplify [] rl G. Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) := - match goal with [|- ?G] => field_lookup Field_simplify [lH] rl [G] end. + let G := Get_goal in + field_lookup Field_simplify [lH] rl G. Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= - let G := getGoal in - let t := type of H in - let g := fresh "goal" in - set (g:= G); - generalize H;clear H; - field_lookup 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 := getGoal in - let t := type of H in - let g := fresh "goal" in - set (g:= G); - generalize H;clear H; - field_lookup Field_simplify [lH] rl [t]; - intro H; - unfold g;clear g. + let G := Get_goal in + let t := type of H in + let g := fresh "goal" in + set (g:= G); + generalize H;clear H; + field_lookup 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); + generalize H;clear H; + field_lookup Field_simplify [lH] rl t; + intro H; + unfold g;clear g. (* Ltac Field_simplify_in hyp:= @@ -176,12 +178,12 @@ Ltac Field_simplify_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]. + 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]. + field_lookup (Field_simplify_in h) [lH] rl t. *) (** Generic tactic for solving equations *) @@ -224,7 +226,7 @@ Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH := [ Simpl_tac | apply Cond_lemma; simpl_PCond req]); clear vlpe nlemma in OnEquation req Main_eq in - ParseFieldComponents lemma Main. + ParseFieldComponents lemma req Main. (* solve completely a field equation, leaving non-zero conditions to be proved (field) *) @@ -239,14 +241,15 @@ Ltac FIELD := post(). Tactic Notation (at level 0) "field" := - let G := getGoal in field_lookup FIELD [] [G]. + let G := Get_goal in + field_lookup FIELD [] G. Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" := - let G := getGoal in field_lookup FIELD [lH] [G]. + let G := Get_goal in + field_lookup 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 := let Simpl := (protect_fv "field") in fun req cst_tac pow_tac _ field_simplify_eq_ok _ _ cond_ok pre post lH rl => @@ -256,17 +259,19 @@ Ltac FIELD_SIMPL := post(). Tactic Notation (at level 0) "field_simplify_eq" := - let G := getGoal in field_lookup FIELD_SIMPL [] [G]. + let G := Get_goal in + field_lookup FIELD_SIMPL [] G. Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := - let G := getGoal in field_lookup FIELD_SIMPL [lH] [G]. + let G := Get_goal in + field_lookup FIELD_SIMPL [lH] G. (* Same as FIELD_SIMPL but in hypothesis *) Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH := let Main radd rmul rsub ropp rdiv rinv rpow C := let hyp := fresh "hyp" in - intro hyp; + intro hyp; match type of hyp with | req ?t1 ?t2 => let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in @@ -306,7 +311,7 @@ Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH := clear hyp end) end in - ParseFieldComponents lemma Main. + ParseFieldComponents lemma req Main. Ltac FIELD_SIMPL_EQ := fun req cst_tac pow_tac _ _ _ lemma cond_ok pre post lH rl => @@ -318,7 +323,7 @@ Ltac FIELD_SIMPL_EQ := Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := let t := type of H in generalize H; - field_lookup FIELD_SIMPL_EQ [] [t]; + field_lookup FIELD_SIMPL_EQ [] t; [ try exact I | clear H;intro H]. @@ -327,7 +332,7 @@ Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) := let t := type of H in generalize H; - field_lookup FIELD_SIMPL_EQ [lH] [t]; + field_lookup FIELD_SIMPL_EQ [lH] t; [ try exact I |clear H;intro H]. @@ -347,59 +352,55 @@ Ltac coerce_to_almost_field set ext f := | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f) end. -Ltac field_elements set ext fspec pspec sspec rk := +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 rk - ltac:(fun arth ext_r morph p_spec s_spec f => f afth ext_r morph p_spec s_spec). - -Ltac field_lemmas set ext inv_m fspec pspec sspec rk := - let simpl_eq_lemma := - match pspec with - | None => constr:(Field_simplify_eq_correct) - | Some _ => constr:(Field_simplify_eq_pow_correct) - end in - let simpl_eq_in_lemma := - match pspec with - | None => constr:(Field_simplify_eq_in_correct) - | Some _ => constr:(Field_simplify_eq_pow_in_correct) - end in - let rw_lemma := - match pspec with - | None => constr:(Field_rw_correct) - | Some _ => constr:(Field_rw_pow_correct) - end in - field_elements set ext fspec pspec sspec rk - ltac:(fun afth ext_r morph p_spec s_spec => - match p_spec with - | mkhypo ?pp_spec => match s_spec with - | mkhypo ?ss_spec => - let field_simpl_eq_ok := - constr:(simpl_eq_lemma _ _ _ _ _ _ _ _ _ _ + 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 => + let field_ok3 := constr:(field_ok2 _ ss_spec) in + match d_spec with + | mkhypo ?dd_spec => + let field_ok := constr:(field_ok3 _ dd_spec) in + let mk_lemma lemma := + constr:(lemma _ _ _ _ _ _ _ _ _ _ set ext_r inv_m afth _ _ _ _ _ _ _ _ _ morph - _ _ _ pp_spec _ ss_spec) in - let field_simpl_ok := - constr:(rw_lemma _ _ _ _ _ _ _ _ _ _ - set ext_r inv_m afth - _ _ _ _ _ _ _ _ _ morph - _ _ _ pp_spec _ ss_spec) in - let field_simpl_eq_in := - constr:(simpl_eq_in_lemma _ _ _ _ _ _ _ _ _ _ - set ext_r inv_m afth - _ _ _ _ _ _ _ _ _ morph - _ _ _ pp_spec _ ss_spec) in - let field_ok := - constr:(Field_correct set ext_r inv_m afth morph pp_spec ss_spec) in - let cond1_ok := - constr:(Pcond_simpl_gen set ext_r afth morph pp_spec) in - let cond2_ok := - constr:(Pcond_simpl_complete set ext_r afth morph pp_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 2 "bad sign specification" - end - | _ => fail 1 "bad power specification" + _ _ _ 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 coefficiant 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). - |