Skip to content

Commit 8d8cd91

Browse files
proux01proux01
committed
Prepare move of micromega_checker.v to Corelib
1 parent b609371 commit 8d8cd91

File tree

8 files changed

+903
-699
lines changed

8 files changed

+903
-699
lines changed

‎test-suite/output/MExtraction.v‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
Don't forget to update it in Rocq core when editing this MExtraction.v file
1919
or MExtraction.out *)
2020

21+
From Stdlib Require Import micromega_checker.
2122
From Stdlib Require Extraction.
2223
From Stdlib Require Import ZMicromega.
2324
From Stdlib Require Import QMicromega.

‎theories/micromega/EnvRing.v‎

Lines changed: 25 additions & 292 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
I have modified the code to use binary trees -- logarithmic access. *)
1313

1414
From Stdlib Require Export micromega_formula micromega_witness.
15+
From Stdlib Require Export micromega_checker.
1516
From Stdlib Require Import Setoid Morphisms Env BinPos BinNat BinInt.
1617
From Stdlib Require Export Ring_theory.
1718

@@ -103,275 +104,34 @@ Section MakeRingPol.
103104
Implicit Types pe : PExpr.
104105
Implicit Types P : Pol.
105106

106-
Definition P0 := Pc cO.
107-
Definition P1 := Pc cI.
108-
109-
Fixpoint Peq (P P' : Pol) {struct P'} : bool :=
110-
match P, P' with
111-
| Pc c, Pc c' => c ?=! c'
112-
| Pinj j Q, Pinj j' Q' =>
113-
match j ?= j' with
114-
| Eq => Peq Q Q'
115-
| _ => false
116-
end
117-
| PX P i Q, PX P' i' Q' =>
118-
match i ?= i' with
119-
| Eq => if Peq P P' then Peq Q Q' else false
120-
| _ => false
121-
end
122-
| _, _ => false
123-
end.
107+
#[local] Notation P0 := (P0 cO).
108+
#[local] Notation P1 := (P1 cI).
109+
#[local] Notation Peq := (Peq ceqb).
110+
#[local] Notation mkPX := (mkPX cO ceqb).
111+
#[local] Notation mk_X := (mkX cO cI).
112+
#[local] Notation Popp := (Popp copp).
113+
#[local] Notation PaddC := (PaddC cadd).
114+
#[local] Notation PsubC := (PsubC csub).
115+
#[local] Notation PaddI := (PaddI cadd).
116+
#[local] Notation PaddX := (PaddX cO ceqb).
117+
#[local] Notation Padd := (Padd cO cadd ceqb).
118+
#[local] Notation PsubI := (PsubI cadd copp).
119+
#[local] Notation PsubX := (PsubX cO copp ceqb).
120+
#[local] Notation Psub := (Psub cO cadd csub copp ceqb).
121+
#[local] Notation PmulC_aux := (PmulC_aux cO cmul ceqb).
122+
#[local] Notation PmulC := (PmulC cO cI cmul ceqb).
123+
#[local] Notation PmulI := (PmulI cO cI cmul ceqb).
124+
#[local] Notation Pmul := (Pmul cO cI cadd cmul ceqb).
125+
#[local] Notation Psquare := (Psquare cO cI cadd cmul ceqb).
126+
#[local] Notation Ppow_pos := (Ppow_pos cO cI cadd cmul ceqb).
127+
#[local] Notation norm_aux := (Pol_of_PExpr cO cI cadd cmul csub copp ceqb).
124128

125129
Infix "?==" := Peq.
126-
127-
Definition mkPinj j P :=
128-
match P with
129-
| Pc _ => P
130-
| Pinj j' Q => Pinj (j + j') Q
131-
| _ => Pinj j P
132-
end.
133-
134-
Definition mkPinj_pred j P :=
135-
match j with
136-
| xH => P
137-
| xO j => Pinj (Pos.pred_double j) P
138-
| xI j => Pinj (xO j) P
139-
end.
140-
141-
Definition mkPX P i Q :=
142-
match P with
143-
| Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q
144-
| Pinj _ _ => PX P i Q
145-
| PX P' i' Q' => if Q' ?== P0 then PX P' (i' + i) Q else PX P i Q
146-
end.
147-
148-
Definition mkXi i := PX P1 i P0.
149-
150-
Definition mkX := mkXi 1.
151-
152-
(** Opposite of addition *)
153-
154-
Fixpoint Popp (P:Pol) : Pol :=
155-
match P with
156-
| Pc c => Pc (-! c)
157-
| Pinj j Q => Pinj j (Popp Q)
158-
| PX P i Q => PX (Popp P) i (Popp Q)
159-
end.
160-
161130
Notation "-- P" := (Popp P).
162-
163-
(** Addition et subtraction *)
164-
165-
Fixpoint PaddC (P:Pol) (c:C) : Pol :=
166-
match P with
167-
| Pc c1 => Pc (c1 +! c)
168-
| Pinj j Q => Pinj j (PaddC Q c)
169-
| PX P i Q => PX P i (PaddC Q c)
170-
end.
171-
172-
Fixpoint PsubC (P:Pol) (c:C) : Pol :=
173-
match P with
174-
| Pc c1 => Pc (c1 -! c)
175-
| Pinj j Q => Pinj j (PsubC Q c)
176-
| PX P i Q => PX P i (PsubC Q c)
177-
end.
178-
179-
Section PopI.
180-
181-
Variable Pop : Pol -> Pol -> Pol.
182-
Variable Q : Pol.
183-
184-
Fixpoint PaddI (j:positive) (P:Pol) : Pol :=
185-
match P with
186-
| Pc c => mkPinj j (PaddC Q c)
187-
| Pinj j' Q' =>
188-
match Z.pos_sub j' j with
189-
| Zpos k => mkPinj j (Pop (Pinj k Q') Q)
190-
| Z0 => mkPinj j (Pop Q' Q)
191-
| Zneg k => mkPinj j' (PaddI k Q')
192-
end
193-
| PX P i Q' =>
194-
match j with
195-
| xH => PX P i (Pop Q' Q)
196-
| xO j => PX P i (PaddI (Pos.pred_double j) Q')
197-
| xI j => PX P i (PaddI (xO j) Q')
198-
end
199-
end.
200-
201-
Fixpoint PsubI (j:positive) (P:Pol) : Pol :=
202-
match P with
203-
| Pc c => mkPinj j (PaddC (--Q) c)
204-
| Pinj j' Q' =>
205-
match Z.pos_sub j' j with
206-
| Zpos k => mkPinj j (Pop (Pinj k Q') Q)
207-
| Z0 => mkPinj j (Pop Q' Q)
208-
| Zneg k => mkPinj j' (PsubI k Q')
209-
end
210-
| PX P i Q' =>
211-
match j with
212-
| xH => PX P i (Pop Q' Q)
213-
| xO j => PX P i (PsubI (Pos.pred_double j) Q')
214-
| xI j => PX P i (PsubI (xO j) Q')
215-
end
216-
end.
217-
218-
Variable P' : Pol.
219-
220-
Fixpoint PaddX (i':positive) (P:Pol) : Pol :=
221-
match P with
222-
| Pc c => PX P' i' P
223-
| Pinj j Q' =>
224-
match j with
225-
| xH => PX P' i' Q'
226-
| xO j => PX P' i' (Pinj (Pos.pred_double j) Q')
227-
| xI j => PX P' i' (Pinj (xO j) Q')
228-
end
229-
| PX P i Q' =>
230-
match Z.pos_sub i i' with
231-
| Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
232-
| Z0 => mkPX (Pop P P') i Q'
233-
| Zneg k => mkPX (PaddX k P) i Q'
234-
end
235-
end.
236-
237-
Fixpoint PsubX (i':positive) (P:Pol) : Pol :=
238-
match P with
239-
| Pc c => PX (--P') i' P
240-
| Pinj j Q' =>
241-
match j with
242-
| xH => PX (--P') i' Q'
243-
| xO j => PX (--P') i' (Pinj (Pos.pred_double j) Q')
244-
| xI j => PX (--P') i' (Pinj (xO j) Q')
245-
end
246-
| PX P i Q' =>
247-
match Z.pos_sub i i' with
248-
| Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
249-
| Z0 => mkPX (Pop P P') i Q'
250-
| Zneg k => mkPX (PsubX k P) i Q'
251-
end
252-
end.
253-
254-
255-
End PopI.
256-
257-
Fixpoint Padd (P P': Pol) {struct P'} : Pol :=
258-
match P' with
259-
| Pc c' => PaddC P c'
260-
| Pinj j' Q' => PaddI Padd Q' j' P
261-
| PX P' i' Q' =>
262-
match P with
263-
| Pc c => PX P' i' (PaddC Q' c)
264-
| Pinj j Q =>
265-
match j with
266-
| xH => PX P' i' (Padd Q Q')
267-
| xO j => PX P' i' (Padd (Pinj (Pos.pred_double j) Q) Q')
268-
| xI j => PX P' i' (Padd (Pinj (xO j) Q) Q')
269-
end
270-
| PX P i Q =>
271-
match Z.pos_sub i i' with
272-
| Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q')
273-
| Z0 => mkPX (Padd P P') i (Padd Q Q')
274-
| Zneg k => mkPX (PaddX Padd P' k P) i (Padd Q Q')
275-
end
276-
end
277-
end.
278131
Infix "++" := Padd.
279-
280-
Fixpoint Psub (P P': Pol) {struct P'} : Pol :=
281-
match P' with
282-
| Pc c' => PsubC P c'
283-
| Pinj j' Q' => PsubI Psub Q' j' P
284-
| PX P' i' Q' =>
285-
match P with
286-
| Pc c => PX (--P') i' (*(--(PsubC Q' c))*) (PaddC (--Q') c)
287-
| Pinj j Q =>
288-
match j with
289-
| xH => PX (--P') i' (Psub Q Q')
290-
| xO j => PX (--P') i' (Psub (Pinj (Pos.pred_double j) Q) Q')
291-
| xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q')
292-
end
293-
| PX P i Q =>
294-
match Z.pos_sub i i' with
295-
| Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q')
296-
| Z0 => mkPX (Psub P P') i (Psub Q Q')
297-
| Zneg k => mkPX (PsubX Psub P' k P) i (Psub Q Q')
298-
end
299-
end
300-
end.
301132
Infix "--" := Psub.
302-
303-
(** Multiplication *)
304-
305-
Fixpoint PmulC_aux (P:Pol) (c:C) : Pol :=
306-
match P with
307-
| Pc c' => Pc (c' *! c)
308-
| Pinj j Q => mkPinj j (PmulC_aux Q c)
309-
| PX P i Q => mkPX (PmulC_aux P c) i (PmulC_aux Q c)
310-
end.
311-
312-
Definition PmulC P c :=
313-
if c ?=! cO then P0 else
314-
if c ?=! cI then P else PmulC_aux P c.
315-
316-
Section PmulI.
317-
Variable Pmul : Pol -> Pol -> Pol.
318-
Variable Q : Pol.
319-
Fixpoint PmulI (j:positive) (P:Pol) : Pol :=
320-
match P with
321-
| Pc c => mkPinj j (PmulC Q c)
322-
| Pinj j' Q' =>
323-
match Z.pos_sub j' j with
324-
| Zpos k => mkPinj j (Pmul (Pinj k Q') Q)
325-
| Z0 => mkPinj j (Pmul Q' Q)
326-
| Zneg k => mkPinj j' (PmulI k Q')
327-
end
328-
| PX P' i' Q' =>
329-
match j with
330-
| xH => mkPX (PmulI xH P') i' (Pmul Q' Q)
331-
| xO j' => mkPX (PmulI j P') i' (PmulI (Pos.pred_double j') Q')
332-
| xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q')
333-
end
334-
end.
335-
336-
End PmulI.
337-
338-
Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol :=
339-
match P'' with
340-
| Pc c => PmulC P c
341-
| Pinj j' Q' => PmulI Pmul Q' j' P
342-
| PX P' i' Q' =>
343-
match P with
344-
| Pc c => PmulC P'' c
345-
| Pinj j Q =>
346-
let QQ' :=
347-
match j with
348-
| xH => Pmul Q Q'
349-
| xO j => Pmul (Pinj (Pos.pred_double j) Q) Q'
350-
| xI j => Pmul (Pinj (xO j) Q) Q'
351-
end in
352-
mkPX (Pmul P P') i' QQ'
353-
| PX P i Q=>
354-
let QQ' := Pmul Q Q' in
355-
let PQ' := PmulI Pmul Q' xH P in
356-
let QP' := Pmul (mkPinj xH Q) P' in
357-
let PP' := Pmul P P' in
358-
(mkPX (mkPX PP' i P0 ++ QP') i' P0) ++ mkPX PQ' i QQ'
359-
end
360-
end.
361-
362133
Infix "**" := Pmul.
363134

364-
Fixpoint Psquare (P:Pol) : Pol :=
365-
match P with
366-
| Pc c => Pc (c *! c)
367-
| Pinj j Q => Pinj j (Psquare Q)
368-
| PX P i Q =>
369-
let twoPQ := Pmul P (mkPinj xH (PmulC Q (cI +! cI))) in
370-
let Q2 := Psquare Q in
371-
let P2 := Psquare P in
372-
mkPX (mkPX P2 i P0 ++ twoPQ) i Q2
373-
end.
374-
375135
(** Monomial **)
376136

377137
(** A monomial is X1^k1...Xi^ki. Its representation
@@ -919,9 +679,6 @@ Qed.
919679
rewrite <- IHm; auto.
920680
Qed.
921681

922-
(** evaluation of polynomial expressions towards R *)
923-
Definition mk_X j := mkPinj_pred j mkX.
924-
925682
(** evaluation of polynomial expressions towards R *)
926683

927684
Fixpoint PEeval (l:Env R) (pe:PExpr) : R :=
@@ -949,18 +706,6 @@ Qed.
949706

950707
Section POWER.
951708
Variable subst_l : Pol -> Pol.
952-
Fixpoint Ppow_pos (res P:Pol) (p:positive) : Pol :=
953-
match p with
954-
| xH => subst_l (res ** P)
955-
| xO p => Ppow_pos (Ppow_pos res P p) P p
956-
| xI p => subst_l ((Ppow_pos (Ppow_pos res P p) P p) ** P)
957-
end.
958-
959-
Definition Ppow_N P n :=
960-
match n with
961-
| N0 => P1
962-
| Npos p => Ppow_pos P1 P p
963-
end.
964709

965710
Lemma Ppow_pos_ok l :
966711
(forall P, subst_l P@l == P@l) ->
@@ -971,6 +716,8 @@ Section POWER.
971716
mul_permut.
972717
Qed.
973718

719+
#[local] Notation Ppow_N := (Ppow_N cO cI cadd cmul ceqb).
720+
974721
Lemma Ppow_N_ok l :
975722
(forall P, subst_l P@l == P@l) ->
976723
forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
@@ -991,20 +738,6 @@ Section POWER.
991738
Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
992739
Let Ppow_subst := Ppow_N subst_l.
993740

994-
Fixpoint norm_aux (pe:PExpr) : Pol :=
995-
match pe with
996-
| PEc c => Pc c
997-
| PEX j => mk_X j
998-
| PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1)
999-
| PEadd pe1 (PEopp pe2) =>
1000-
Psub (norm_aux pe1) (norm_aux pe2)
1001-
| PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2)
1002-
| PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
1003-
| PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2)
1004-
| PEopp pe1 => Popp (norm_aux pe1)
1005-
| PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
1006-
end.
1007-
1008741
Definition norm_subst pe := subst_l (norm_aux pe).
1009742

1010743
(** Internally, [norm_aux] is expanded in a large number of cases.
@@ -1053,7 +786,7 @@ Section POWER.
1053786
- simpl. rewrite IHpe1, IHpe2. Esimpl.
1054787
- simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok.
1055788
- simpl. rewrite IHpe. Esimpl.
1056-
- simpl. rewrite Ppow_N_ok by reflexivity.
789+
- simpl. rewrite (Ppow_N_ok id) by reflexivity.
1057790
rewrite (rpow_pow_N pow_th). destruct n0 as [|p]; simpl; Esimpl.
1058791
induction p as [p IHp|p IHp|];simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok.
1059792
Qed.

0 commit comments

Comments
 (0)