Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Revert "Workaround for #87" #99

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Revert "Workaround for #87" #99

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
59 changes: 28 additions & 31 deletions theories/ring.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
From elpi Require Import elpi.
From Coq Require Import ZArith Ring Ring_polynom Field_theory.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.

Check warning on line 3 in theories/ring.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

Hiding binding of key N to N_scope

Check warning on line 3 in theories/ring.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18) 

Hiding binding of key N to N_scope
From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.

Check warning on line 4 in theories/ring.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

Hiding binding of key Z to Z_scope

Check warning on line 4 in theories/ring.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.18) 

Hiding binding of key Z to Z_scope

Check warning on line 4 in theories/ring.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-dev) 

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

Check warning on line 4 in theories/ring.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-dev) 

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
From mathcomp.zify Require Import ssrZ zify.
From mathcomp.algebra_tactics Require Import common.
From mathcomp.algebra_tactics Extra Dependency "common.elpi" as common.
Expand Down Expand Up @@ -163,16 +163,15 @@
(lpe : seq (RExpr R * RExpr R * PExpr Z * PExpr Z))
(re1 re2 : RExpr R) (pe1 pe2 : PExpr Z) :
Reval_eqs lpe ->
(* FIXME: workaround for #87 *)
(forall R_of_Z zero opp add sub_ one mul exp,
Ring.Rnorm R_of_Z zero add opp sub_ one mul exp
(forall R_of_Z zero opp add sub one mul exp,
Ring.Rnorm R_of_Z zero add opp sub one mul exp
(@target_comRingMorph R) re1 ::
Ring.Rnorm R_of_Z zero add opp sub_ one mul exp
Ring.Rnorm R_of_Z zero add opp sub one mul exp
(@target_comRingMorph R) re2 ::
Rnorm_list R_of_Z zero add opp sub_ one mul exp lpe =
PEeval zero one add mul sub_ opp R_of_Z id exp l pe1 ::
PEeval zero one add mul sub_ opp R_of_Z id exp l pe2 ::
PEeval_list R_of_Z zero opp add sub_ one mul exp l lpe) ->
Rnorm_list R_of_Z zero add opp sub one mul exp lpe =
PEeval zero one add mul sub opp R_of_Z id exp l pe1 ::
PEeval zero one add mul sub opp R_of_Z id exp l pe2 ::
PEeval_list R_of_Z zero opp add sub one mul exp l lpe) ->
(let norm_subst' :=
norm_subst 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb (triv_div 0 1 Z.eqb) n
(mk_monpol_list
Expand Down Expand Up @@ -255,18 +254,17 @@
(lpe : seq (RExpr F * RExpr F * PExpr Z * PExpr Z))
(re1 re2 : RExpr F) (fe1 fe2 : FExpr Z) :
Reval_eqs lpe ->
(* FIXME: workaround for #87 *)
(forall R_of_Z zero opp add sub_ one mul exp div inv,
Field.Rnorm R_of_Z zero add opp sub_ one mul exp inv id re1 ::
Field.Rnorm R_of_Z zero add opp sub_ one mul exp inv id re2 ::
Rnorm_list R_of_Z zero add opp sub_ one mul exp lpe =
FEeval zero one add mul sub_ opp div inv R_of_Z id exp l fe1 ::
FEeval zero one add mul sub_ opp div inv R_of_Z id exp l fe2 ::
PEeval_list R_of_Z zero opp add sub_ one mul exp l lpe) ->
(forall is_true_ negb_ andb_ zero one add mul sub_ opp Feqb F_of_nat exp l',
(forall R_of_Z zero opp add sub one mul exp div inv,
Field.Rnorm R_of_Z zero add opp sub one mul exp inv id re1 ::
Field.Rnorm R_of_Z zero add opp sub one mul exp inv id re2 ::
Rnorm_list R_of_Z zero add opp sub one mul exp lpe =
FEeval zero one add mul sub opp div inv R_of_Z id exp l fe1 ::
FEeval zero one add mul sub opp div inv R_of_Z id exp l fe2 ::
PEeval_list R_of_Z zero opp add sub one mul exp l lpe) ->
(forall is_true_ negb_ andb_ zero one add mul sub opp Feqb F_of_nat exp l',
is_true_ = is_true -> negb_ = negb -> andb_ = andb ->
zero = 0 -> one = 1 -> add = +%R -> mul = *%R ->
sub_ = (fun x y => x - y) -> opp = -%R -> Feqb = eq_op ->
sub = (fun x y => x - y) -> opp = -%R -> Feqb = eq_op ->
F_of_nat = GRing.natmul 1 -> exp = @GRing.exp F -> l' = l ->
let F_of_pos p := if p is xH then one else F_of_nat (Pos.to_nat p) in
let F_of_Z n :=
Expand All @@ -285,7 +283,7 @@
Peq Z.eqb (norm_subst' (PEmul (num nfe1) (denum nfe2)))
(norm_subst' (PEmul (num nfe2) (denum nfe1))) /\
is_true_ (PCond' true negb_ andb_
zero one add mul sub_ opp Feqb F_of_Z nat_of_N exp l'
zero one add mul sub opp Feqb F_of_Z nat_of_N exp l'
(Fapp (Fcons00 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb
(triv_div 0 1 Z.eqb))
(condition nfe1 ++ condition nfe2) [::]))) ->
Expand All @@ -310,18 +308,17 @@
(lpe : seq (RExpr F * RExpr F * PExpr Z * PExpr Z))
(re1 re2 : RExpr F) (fe1 fe2 : FExpr Z) :
Reval_eqs lpe ->
(* FIXME: workaround for #87 *)
(forall R_of_Z zero opp add sub_ one mul exp div inv,
Field.Rnorm R_of_Z zero add opp sub_ one mul exp inv id re1 ::
Field.Rnorm R_of_Z zero add opp sub_ one mul exp inv id re2 ::
Rnorm_list R_of_Z zero add opp sub_ one mul exp lpe =
FEeval zero one add mul sub_ opp div inv R_of_Z id exp l fe1 ::
FEeval zero one add mul sub_ opp div inv R_of_Z id exp l fe2 ::
PEeval_list R_of_Z zero opp add sub_ one mul exp l lpe) ->
(forall is_true_ negb_ andb_ zero one add mul sub_ opp Feqb F_of_nat exp l',
(forall R_of_Z zero opp add sub one mul exp div inv,
Field.Rnorm R_of_Z zero add opp sub one mul exp inv id re1 ::
Field.Rnorm R_of_Z zero add opp sub one mul exp inv id re2 ::
Rnorm_list R_of_Z zero add opp sub one mul exp lpe =
FEeval zero one add mul sub opp div inv R_of_Z id exp l fe1 ::
FEeval zero one add mul sub opp div inv R_of_Z id exp l fe2 ::
PEeval_list R_of_Z zero opp add sub one mul exp l lpe) ->
(forall is_true_ negb_ andb_ zero one add mul sub opp Feqb F_of_nat exp l',
is_true_ = is_true -> negb_ = negb -> andb_ = andb ->
zero = 0 -> one = 1 -> add = +%R -> mul = *%R ->
sub_ = (fun x y => x - y) -> opp = -%R -> Feqb = eq_op ->
sub = (fun x y => x - y) -> opp = -%R -> Feqb = eq_op ->
F_of_nat = GRing.natmul 1 -> exp = @GRing.exp F -> l' = l ->
let F_of_pos p := if p is xH then one else F_of_nat (Pos.to_nat p) in
let F_of_Z n :=
Expand All @@ -340,7 +337,7 @@
Peq Z.eqb (norm_subst' (PEmul (num nfe1) (denum nfe2)))
(norm_subst' (PEmul (num nfe2) (denum nfe1))) /\
is_true_ (PCond' true negb_ andb_
zero one add mul sub_ opp Feqb F_of_Z nat_of_N exp l'
zero one add mul sub opp Feqb F_of_Z nat_of_N exp l'
(Fapp (Fcons2 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb
(triv_div 0 1 Z.eqb))
(condition nfe1 ++ condition nfe2) [::]))) ->
Expand Down Expand Up @@ -375,7 +372,7 @@
let one := fresh "one" in
let add := fresh "add" in
let mul := fresh "mul" in
let sub := fresh "sub_" in (* FIXME: workaround for #87 *)
let sub := fresh "sub" in
let opp := fresh "opp" in
let Feqb := fresh "Feqb" in
let F_of_nat := fresh "F_of_nat" in
Expand Down