diff --git a/examples/lra_examples.v b/examples/lra_examples.v index f2e6798..70eff07 100644 --- a/examples/lra_examples.v +++ b/examples/lra_examples.v @@ -258,8 +258,8 @@ Qed. Goal ratr (1 / 2%:R) = 1 / 2%:R :> F. Proof. -Fail lra. (* TODO should work *) -Abort. +lra. +Qed. Goal 1 ^+ (2 + 2) = 1 :> F. Proof. diff --git a/theories/lra.elpi b/theories/lra.elpi index c00cbb0..0bd9483 100644 --- a/theories/lra.elpi +++ b/theories/lra.elpi @@ -61,19 +61,24 @@ pred rf->porder o:rf, o:term. rf->porder (field F) T :- coq.unify-eq {{ Num.RealField.porderType lp:F }} T ok. rf->porder (ring R) T :- coq.unify-eq {{ Num.RealDomain.porderType lp:R }} T ok. -pred rf->zmod o:rf, o:term. -rf->zmod (field F) T :- coq.unify-eq {{ Num.RealField.zmodType lp:F }} T ok. -rf->zmod (ring R) T :- coq.unify-eq {{ Num.RealDomain.zmodType lp:R }} T ok. - pred rf->ring o:rf, o:term. rf->ring (field F) T :- coq.unify-eq {{ Num.RealField.ringType lp:F }} T ok. rf->ring (ring R) T :- coq.unify-eq {{ Num.RealDomain.ringType lp:R }} T ok. -pred rf->unitRing o:rf, o:term. -rf->unitRing (field F) T :- - coq.unify-eq {{ Num.RealField.unitRingType lp:F }} T ok. -rf->unitRing (ring R) T :- - coq.unify-eq {{ Num.RealDomain.unitRingType lp:R }} T ok. +pred rf->numDomain o:rf, o:term. +rf->numDomain (field F) D :- + coq.unify-eq {{ Num.RealField.numDomainType lp:F }} D ok. +rf->numDomain (ring R) D :- + coq.unify-eq {{ Num.RealDomain.numDomainType lp:R }} D ok. + +pred field->unitRing o:term, o:term. +field->unitRing F U :- coq.unify-eq {{ GRing.Field.unitRingType lp:F }} U ok. + +pred unitRing->ring o:term, o:term. +unitRing->ring U R :- coq.unify-eq {{ GRing.UnitRing.ringType lp:U }} R ok. + +pred ring->zmod o:term, o:term. +ring->zmod R T :- coq.unify-eq {{ GRing.Ring.zmodType lp:R }} T ok. % [field-mode] is true if we are on a realFieldType, % otherwise we are on a realDomainType. @@ -132,120 +137,186 @@ rfstr _ _ _ :- coq.ltac.fail _ "Cannot find a realDomainType". %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Reification procedure -% [quote.cstr F In Out] reifies integer constants -% - [F] is a [realDomainType] or [realFieldType] instance, -% - [In] is a term of type [F], -% - [Out] is a reified constant of type [Z] -pred quote.cstr i:rf, i:term, o:term. -quote.cstr F {{ GRing.zero lp:Z }} {{ Z0 }} :- rf->zmod F Z. -quote.cstr F {{ GRing.one lp:R }} {{ (Zpos 1) }} :- rf->ring F R. -quote.cstr F {{ @GRing.natmul lp:Z (GRing.one lp:R) lp:X }} XZ :- - rf->zmod F Z, rf->ring F R, nat->Z X XZ. - -% [quote.cstf F In Out] reifies rational constants -% - [F] is a [realFieldType] instance, -% - [In] is a term of type [F], -% - [Out] is a reified constant of type [Q] -pred quote.cstf i:rf, i:term, o:term. -quote.cstf F {{ @GRing.inv lp:U (@GRing.natmul lp:Z (GRing.one lp:R) lp:X) }} - E' :- rf->unitRing F U, rf->zmod F Z, rf->ring F R, - nat->N X XN, XN = {{ Npos lp:XP }}, !, E' = {{ Qmake 1 lp:XP }}. - -% [quote.expr F In Out VarMap] reifies arithmetic expressions +% [quote.cstr V In OutM Out] reifies integer constants +% - [V] is a [ringType] +% - [In] is a term of type [V], +% - [OutM] is a reified constant of type [MExpr V] +% - [Out] is a reified constant of type [PExpr Q] +pred quote.cstr i:term, i:term, o:term, o:term. +quote.cstr V {{ GRing.zero lp:Z }} OutM Out :- ring->zmod V Z, + OutM = {{ @Internals.MEint lp:V Z0 }}, Out = {{ PEc (Qmake Z0 1) }}. +quote.cstr V {{ GRing.one lp:V' }} OutM Out :- coq.unify-eq V V' ok, + OutM = {{ @Internals.MEint lp:V (Zpos 1) }}, Out = {{ PEc (Qmake 1 1) }}. +quote.cstr V {{ @GRing.natmul lp:Z (GRing.one lp:V') lp:X }} OutM Out :- + ring->zmod V Z, coq.unify-eq V V' ok, nat->Z X XZ, + OutM = {{ @Internals.MEint lp:V lp:XZ }}, Out = {{ PEc (Qmake lp:XZ 1) }}. + +% [quote.cstf V In OutM Out] reifies rational constants +% - [V] is a [ringType] instance, +% - [In] is a term of type [V], +% - [OutM] is a reified constant of type [MExpr V] +% - [Out] is a reified constant of type [PExpr Q] +pred quote.cstf i:term, i:term, o:term, o:term. +quote.cstf V {{ @GRing.inv lp:U (@GRing.natmul lp:Z (GRing.one lp:V') lp:X) }} + OutM Out :- unitRing->ring U V, ring->zmod V Z, coq.unify-eq V V' ok, + nat->N X XN, XN = {{ Npos lp:XP }}, XQ = {{ Qmake 1 lp:XP }}, + field->unitRing F U, + OutM = {{ @Internals.MErat lp:F lp:XQ }}, Out = {{ PEc lp:XQ }}. + +% [quote.expr V F In OutM Out VM] reifies arithmetic expressions +% - [V] is a [ringType] +% - [F] is a function +% - [In] is a term of type [V], +% - [OutM] is a reified expression of type [MExpr V] +% - [Out] is a reified expression of type [PExpr Q] +% - [VM] is a variable map, that is a list of terms of type [V]. +pred quote.expr i:term, i:(term -> term), i:term, o:term, o:term, o:list term. +quote.expr V F {{ @GRing.add lp:Z lp:In1 lp:In2 }} OutM Out VM :- + ring->zmod V Z, !, + quote.expr V F In1 OutM1 Out1 VM, !, quote.expr V F In2 OutM2 Out2 VM, !, + OutM = {{ @Internals.MEadd lp:V lp:OutM1 lp:OutM2 }}, + Out = {{ PEadd lp:Out1 lp:Out2 }}. +quote.expr V F {{ @GRing.mul lp:V' lp:In1 lp:In2 }} OutM Out VM :- + coq.unify-eq V V' ok, !, + quote.expr V F In1 OutM1 Out1 VM, !, quote.expr V F In2 OutM2 Out2 VM, !, + OutM = {{ @Internals.MEmul lp:V lp:OutM1 lp:OutM2 }}, + Out = {{ PEmul lp:Out1 lp:Out2 }}. +quote.expr V F {{ @GRing.opp lp:Z lp:In1 }} OutM Out VM :- + ring->zmod V Z, !, + quote.expr V F In1 OutM1 Out1 VM, !, + OutM = {{ @Internals.MEopp lp:V lp:OutM1 }}, Out = {{ PEopp lp:Out1 }}. +quote.expr V F {{ @GRing.exp lp:V' lp:In1 lp:X }} OutM Out VM :- + coq.unify-eq V V' ok, nat->N X XN, !, + quote.expr V F In1 OutM1 Out1 VM, !, + OutM = {{ @Internals.MEpow lp:V lp:OutM1 lp:XN }}, + Out = {{ PEpow lp:Out1 lp:XN }}. +quote.expr V _ In OutM Out _ :- quote.cstr V In OutM Out. +quote.expr V _ In OutM Out _ :- field-mode, quote.cstf V In OutM Out. +quote.expr V F In {{ @Internals.MEmorph lp:U lp:V lp:G lp:OutM }} Out VM :- + coq.unify-eq + {{ @GRing.RMorphism.apply lp:U lp:V lp:Ph lp:G lp:In1 }} In ok, !, + quote.expr U (x\ F {{ @GRing.RMorphism.apply lp:U lp:V lp:Ph lp:G lp:x }}) + In1 OutM Out VM. +quote.expr V F In {{ @Internals.MEX lp:V lp:In }} {{ PEX lp:N }} VM :- !, + mem VM (F In) N. + +% [quote.exprw F In OutM Out VM] reifies arithmetic expressions % - [F] is a [realDomainType] or [realFieldType] instance, % - [In] is a term of type [F], +% - [OutM] is a reified expression of type [MExpr F] % - [Out] is a reified expression of type [PExpr Q] -% - [VarMap] is a variable map, that is a list of terms of type [F]. -pred quote.expr i:rf, i:term, o:term, o:list term. -quote.expr F {{ @GRing.add lp:Z lp:E1 lp:E2 }} E' VM :- rf->zmod F Z, !, - quote.expr F E1 E1' VM, !, quote.expr F E2 E2' VM, !, - E' = {{ PEadd lp:E1' lp:E2' }}. -quote.expr F {{ @GRing.opp lp:Z lp:E }} {{ PEopp lp:E' }} VM :- rf->zmod F Z, !, - quote.expr F E E' VM. -quote.expr F {{ @GRing.mul lp:R lp:E1 lp:E2 }} E' VM :- rf->ring F R, !, - quote.expr F E1 E1' VM, !, quote.expr F E2 E2' VM, !, - E' = {{ PEmul lp:E1' lp:E2' }}. -quote.expr F {{ @GRing.exp lp:R lp:E1 lp:X }} E' VM :- - rf->ring F R, nat->N X XN, !, - quote.expr F E1 E1' VM, E' = {{ PEpow lp:E1' lp:XN }}. -quote.expr F E {{ PEc (Qmake lp:Z 1) }} _ :- quote.cstr F E Z. -quote.expr F E {{ PEc lp:Q }} _ :- F = field _, quote.cstf F E Q. -quote.expr F {{ lp:X : _ }} X' VM :- !, quote.expr F X X' VM. -quote.expr _ X Out VarMap :- !, mem VarMap X N, Out = {{ PEX lp:N }}. - -% [quote.bop2 F In Out VarMap] reifies boolean (in)equalities +% - [VM] is a variable map, that is a list of terms of type [F]. +pred quote.exprw i:rf, i:term, o:term, o:term, o:list term. +quote.exprw F In OutM Out VM :- F = field _, !, + field-mode => quote.expr { rf->ring F } (x\ x) In OutM Out VM. +quote.exprw F In OutM Out VM :- F = ring _, !, + quote.expr { rf->ring F } (x\ x) In OutM Out VM. + +% [quote.bop2 F In OutM Out VM] reifies boolean (in)equalities % - [F] is a [realDomainType] or [realFieldType] instance, % - [In] is a term of type [bool], +% - [OutM] is a reified expression of type [MFormula] % - [Out] is a reified expression of type [Formula Q] -% - [VarMap] is a variable map, that is a list of terms of type [F]. -pred quote.bop2 i:rf, i:term, o:term, o:list term. -quote.bop2 F {{ @Order.le _ lp:O lp:X lp:Y }} F' VM :- rf->porder F O, !, - quote.expr F X X' VM, !, quote.expr F Y Y' VM, !, - F' = {{ Build_Formula lp:X' OpLe lp:Y' }}. -quote.bop2 F {{ @Order.lt _ lp:O lp:X lp:Y }} F' VM :- rf->porder F O, !, - quote.expr F X X' VM, !, quote.expr F Y Y' VM, !, - F' = {{ Build_Formula lp:X' OpLt lp:Y' }}. -quote.bop2 F {{ @eqtype.eq_op lp:T lp:X lp:Y) }} F' VM :- rf->eq F T, !, - quote.expr F X X' VM, !, quote.expr F Y Y' VM, !, - F' = {{ Build_Formula lp:X' OpEq lp:Y' }}. - -% [quote.pop2 F In Out VarMap] reifies (in)equalities of type Prop +% - [VM] is a variable map, that is a list of terms of type [F]. +pred quote.bop2 i:rf, i:term, o:term, o:term, o:list term. +quote.bop2 F {{ @Order.le _ lp:O lp:X lp:Y }} OutM Out VM :- rf->porder F O, !, + quote.exprw F X XM' X' VM, !, quote.exprw F Y YM' Y' VM, !, + OutM = {{ Internals.Build_MFormula lp:XM' OpLe lp:YM' }}, + Out = {{ Build_Formula lp:X' OpLe lp:Y' }}. +quote.bop2 F {{ @Order.lt _ lp:O lp:X lp:Y }} OutM Out VM :- rf->porder F O, !, + quote.exprw F X XM' X' VM, !, quote.exprw F Y YM' Y' VM, !, + OutM = {{ Internals.Build_MFormula lp:XM' OpLt lp:YM' }}, + Out = {{ Build_Formula lp:X' OpLt lp:Y' }}. +quote.bop2 F {{ @eqtype.eq_op lp:T lp:X lp:Y) }} OutM Out VM :- rf->eq F T, !, + quote.exprw F X XM' X' VM, !, quote.exprw F Y YM' Y' VM, !, + OutM = {{ Internals.Build_MFormula lp:XM' OpEq lp:YM' }}, + Out = {{ Build_Formula lp:X' OpEq lp:Y' }}. + +% [quote.pop2 F In OutM Out VM] reifies (in)equalities of type Prop % - [F] is a [realDomainType] or [realFieldType] instance, % - [In] is a term of type [Prop], +% - [OutM] is a reified expression of type [MFormula] % - [Out] is a reified expression of type [Formula Q] -% - [VarMap] is a variable map, that is a list of terms of type [F]. -pred quote.pop2 i:rf, i:term, o:term, o:list term. -quote.pop2 F {{ is_true lp:E }} F' VM :- quote.bop2 F E F' VM. -quote.pop2 F {{ @eq lp:T lp:X lp:Y) }} F' VM :- rf->sort F T, !, - quote.expr F X X' VM, !, quote.expr F Y Y' VM, !, - F' = {{ Build_Formula lp:X' OpEq lp:Y' }}. - -% [quote.bool F In Out VarMap] reifies boolean formulas +% - [VM] is a variable map, that is a list of terms of type [F]. +pred quote.pop2 i:rf, i:term, o:term, o:term, o:list term. +quote.pop2 F {{ is_true lp:E }} OutM Out VM :- quote.bop2 F E OutM Out VM. +quote.pop2 F {{ @eq lp:T lp:X lp:Y) }} OutM Out VM :- rf->sort F T, !, + quote.exprw F X XM' X' VM, !, quote.exprw F Y YM' Y' VM, !, + OutM = {{ Internals.Build_MFormula lp:XM' OpEq lp:YM' }}, + Out = {{ Build_Formula lp:X' OpEq lp:Y' }}. + +% [quote.bool F In OutM Out VM] reifies boolean formulas % - [F] is a [realDomainType] or [realFieldType] instance, % - [In] is a term of type [bool], +% - [OutM] is a reified formula of type [BFormula MFormula Tauto.isBool] % - [Out] is a reified formula of type [BFormula (Formula Q) Tauto.isBool] -% - [VarMap] is a variable map, that is a list of terms of type [F]. -pred quote.bool i:rf, i:term, o:term, o:list term. -quote.bool F {{ lp:F1 ==> lp:F2 }} {{ IMPL lp:F1' None lp:F2' }} VM :- !, - quote.bool F F1 F1' VM, !, quote.bool F F2 F2' VM. -quote.bool F {{ lp:F1 && lp:F2 }} {{ AND lp:F1' lp:F2' }} VM :- !, - quote.bool F F1 F1' VM, !, quote.bool F F2 F2' VM. -quote.bool F {{ lp:F1 || lp:F2 }} {{ OR lp:F1' lp:F2' }} VM :- !, - quote.bool F F1 F1' VM, !, quote.bool F F2 F2' VM. -quote.bool F {{ ~~ lp:F1 }} {{ NOT lp:F1' }} VM :- !, quote.bool F F1 F1' VM. -quote.bool _ {{ true }} {{ TT Tauto.isBool }} _. -quote.bool _ {{ false }} {{ FF Tauto.isBool }} _. -quote.bool F A {{ A Tauto.isBool lp:A' tt }} VM :- quote.bop2 F A A' VM. -quote.bool _ X {{ X Tauto.isBool lp:X }} _. - -% [quote.prop F In Out VarMap] reifies formulas of type Prop +% - [VM] is a variable map, that is a list of terms of type [F]. +pred quote.bool i:rf, i:term, o:term, o:term, o:list term. +quote.bool F {{ lp:F1 ==> lp:F2 }} OutM Out VM :- !, + quote.bool F F1 OutM1 Out1 VM, !, quote.bool F F2 OutM2 Out2 VM, !, + OutM = {{ IMPL lp:OutM1 None lp:OutM2 }}, + Out = {{ IMPL lp:Out1 None lp:Out2 }}. +quote.bool F {{ lp:F1 && lp:F2 }} OutM Out VM :- !, + quote.bool F F1 OutM1 Out1 VM, !, quote.bool F F2 OutM2 Out2 VM, !, + OutM = {{ AND lp:OutM1 lp:OutM2 }}, Out = {{ AND lp:Out1 lp:Out2 }}. +quote.bool F {{ lp:F1 || lp:F2 }} OutM Out VM :- !, + quote.bool F F1 OutM1 Out1 VM, !, quote.bool F F2 OutM2 Out2 VM, !, + OutM = {{ OR lp:OutM1 lp:OutM2 }}, Out = {{ OR lp:Out1 lp:Out2 }}. +quote.bool F {{ ~~ lp:F1 }} OutM Out VM :- !, quote.bool F F1 OutM1 Out1 VM, !, + OutM = {{ NOT lp:OutM1 }}, Out = {{ NOT lp:Out1 }}. +quote.bool _ {{ true }} OutM Out _ :- !, + OutM = {{ TT Tauto.isBool }}, Out = {{ TT Tauto.isBool }}. +quote.bool _ {{ false }} OutM Out _ :- !, + OutM = {{ FF Tauto.isBool }}, Out = {{ FF Tauto.isBool }}. +quote.bool F In OutM Out VM :- quote.bop2 F In OutM' Out' VM, + OutM = {{ A Tauto.isBool lp:OutM' tt }}, + Out = {{ A Tauto.isBool lp:Out' tt }}. +quote.bool _ In OutM Out _ :- + OutM = {{ X Tauto.isBool lp:In }}, Out = {{ X Tauto.isBool lp:In }}. + +% [quote.prop F In OutM Out VM] reifies formulas of type Prop % - [F] is a [realDomainType] or [realFieldType] instance, % - [In] is a term of type [Prop], +% - [OutM] is a reified formula of type [BFormula MFormula Tauto.isProp] % - [Out] is a reified formula of type [BFormula (Formula Q) Tauto.isProp] -% - [VarMap] is a variable map, that is a list of terms of type [F]. -pred quote.prop i:rf, i:term, o:term, o:list term. -quote.prop F {{ lp:F1 -> lp:F2 }} {{ IMPL lp:F1' None lp:F2' }} VM :- !, - quote.prop F F1 F1' VM, !, quote.prop F F2 F2' VM. -quote.prop F {{ iff lp:F1 lp:F2 }} {{ IFF lp:F1' lp:F2' }} VM :- !, - quote.prop F F1 F1' VM, !, quote.prop F F2 F2' VM. -quote.prop F {{ lp:F1 /\ lp:F2 }} {{ AND lp:F1' lp:F2' }} VM :- !, - quote.prop F F1 F1' VM, !, quote.prop F F2 F2' VM. -quote.prop F {{ lp:F1 \/ lp:F2 }} {{ OR lp:F1' lp:F2' }} VM :- !, - quote.prop F F1 F1' VM, !, quote.prop F F2 F2' VM. -quote.prop F {{ ~ lp:F1 }} {{ NOT lp:F1' }} VM :- !, quote.prop F F1 F1' VM. -quote.prop _ {{ True }} {{ TT Tauto.isProp }} _. -quote.prop _ {{ False }} {{ FF Tauto.isProp }} _. -quote.prop F {{ is_true lp:F1 }} {{ EQ lp:F1' (TT Tauto.isBool) }} VM :- !, - quote.bool F F1 F1' VM. -quote.prop F {{ @eq bool lp:F1 lp:F2 }} {{ EQ lp:F1' lp:F2' }} VM :- !, - quote.bool F F1 F1' VM, !, quote.bool F F2 F2' VM. -quote.prop F A {{ A Tauto.isProp lp:A' tt }} VM :- quote.pop2 F A A' VM. -quote.prop _ X {{ X Tauto.isProp lp:X }} _. +% - [VM] is a variable map, that is a list of terms of type [F]. +pred quote.prop i:rf, i:term, o:term, o:term, o:list term. +quote.prop F {{ lp:F1 -> lp:F2 }} OutM Out VM :- !, + quote.prop F F1 OutM1 Out1 VM, !, quote.prop F F2 OutM2 Out2 VM, !, + OutM = {{ IMPL lp:OutM1 None lp:OutM2 }}, + Out = {{ IMPL lp:Out1 None lp:Out2 }}. +quote.prop F {{ iff lp:F1 lp:F2 }} OutM Out VM :- !, + quote.prop F F1 OutM1 Out1 VM, !, quote.prop F F2 OutM2 Out2 VM, !, + OutM = {{ IFF lp:OutM1 lp:OutM2 }}, Out = {{ IFF lp:Out1 lp:Out2 }}. +quote.prop F {{ lp:F1 /\ lp:F2 }} OutM Out VM :- !, + quote.prop F F1 OutM1 Out1 VM, !, quote.prop F F2 OutM2 Out2 VM, !, + OutM = {{ AND lp:OutM1 lp:OutM2 }}, Out = {{ AND lp:Out1 lp:Out2 }}. +quote.prop F {{ lp:F1 \/ lp:F2 }} OutM Out VM :- !, + quote.prop F F1 OutM1 Out1 VM, !, quote.prop F F2 OutM2 Out2 VM, !, + OutM = {{ OR lp:OutM1 lp:OutM2 }}, Out = {{ OR lp:Out1 lp:Out2 }}. +quote.prop F {{ ~ lp:F1 }} OutM Out VM :- !, quote.prop F F1 OutM1 Out1 VM, !, + OutM = {{ NOT lp:OutM1 }}, Out = {{ NOT lp:Out1 }}. +quote.prop _ {{ true }} OutM Out _ :- !, + OutM = {{ TT Tauto.isProp }}, Out = {{ TT Tauto.isProp }}. +quote.prop _ {{ false }} OutM Out _ :- !, + OutM = {{ FF Tauto.isProp }}, Out = {{ FF Tauto.isProp }}. +quote.prop F {{ is_true lp:In1 }} OutM Out VM :- !, + quote.bool F In1 OutM1 Out1 VM, !, + OutM = {{ EQ lp:OutM1 (TT Tauto.isBool) }}, + Out = {{ EQ lp:Out1 (TT Tauto.isBool) }}. +quote.prop F {{ @eq bool lp:In1 lp:In2 }} OutM Out VM :- !, + quote.bool F In1 OutM1 Out1 VM, !, quote.bool F In2 OutM2 Out2 VM, + OutM = {{ EQ lp:OutM1 lp:OutM2 }}, Out = {{ EQ lp:Out1 lp:Out2 }}. +quote.prop F In OutM Out VM :- quote.pop2 F In OutM' Out' VM, + OutM = {{ A Tauto.isProp lp:OutM' tt }}, + Out = {{ A Tauto.isProp lp:Out' tt }}. +quote.prop _ In OutM Out _ :- + OutM = {{ X Tauto.isProp lp:In }}, Out = {{ X Tauto.isProp lp:In }}. % [simplify.bool In Out] reduces a boolean formula to [X _] % when it doesn't contain any arithmetic part -% - [In] is a reified formula of type [BFormula (Formula Q) Tauto.isBool], -% - [Out] is a simplified formula of type [BFormula (Formula Q) Tauto.isBool] +% - [In] is a reified formula of type [BFormula _ Tauto.isBool], +% - [Out] is a simplified formula of type [BFormula _ Tauto.isBool] pred simplify.bool i:term, o:term. simplify.bool {{ IMPL (X _ lp:F1) None (X _ lp:F2) }} F' :- F' = {{ X Tauto.isBool (lp:F1 ==> lp:F2) }}. @@ -265,8 +336,8 @@ simplify.bool X X. % [simplify.prop In Out] reduces a formula to [X _] % when it doesn't contain any arithmetic part -% - [In] is a reified formula of type [BFormula (Formula Q) Tauto.isProp], -% - [Out] is a simplified formula of type [BFormula (Formula Q) Tauto.isProp] +% - [In] is a reified formula of type [BFormula _ Tauto.isProp], +% - [Out] is a simplified formula of type [BFormula _ Tauto.isProp] pred simplify.prop i:term, o:term. simplify.prop {{ IMPL (X _ lp:F1) None (X _ lp:F2) }} F' :- F' = {{ X Tauto.isProp (lp:F1 -> lp:F2) }}. @@ -292,35 +363,42 @@ simplify.prop {{ EQ lp:F1 lp:F2 }} {{ EQ lp:F1' lp:F2' }} :- simplify.bool F1 F1', simplify.bool F2 F2'. simplify.prop X X. -% [quote F In Out VarMap] reifies formulas of type Prop +% [quote F In Out VM] reifies formulas of type Prop % - [F] is a [realDomainType] or [realFieldType] instance, % - [In] is a term of type [Prop], +% - [OutM] is a reified formula of type [BFormula MFormula Tauto.isProp] % - [Out] is a reified formula of type [BFormula (Formula Q) Tauto.isProp] -% - [VarMap] is a variable map, that is a list of terms of type [F]. -pred quote i:rf, i:term, o:term, o:list term. -quote F In Out' VM :- quote.prop F In Out VM, simplify.prop Out Out'. +% - [VM] is a variable map, that is a list of terms of type [F]. +pred quote i:rf, i:term, o:term, o:term, o:list term. +quote F In OutM' Out' VM :- + quote.prop F In OutM Out VM, simplify.prop OutM OutM', simplify.prop Out Out'. -% [quote.hyps F Hyps Goal ReifiedGoal Out ReifiedOut VarMap] reifies hypotheses +% [quote.hyps F Hyps Goal ReifiedGoal Out ReifiedOut VM] reifies hypotheses % - [F] is a [realDomainType] or [realFieldType] instance, % - [Hyps] are hypotheses % - [Goal] is the goal, of type [Prop] +% - [ReifiedGoalM] is the refied goal as a [BFormula MFormula Tauto.isProp] % - [ReifiedGoal] is the refied goal as a [BFormula (Formula Q) Tauto.isProp] % - [Out] is a chain of implications including [Goal] and hypotheses in [Hyps] % that have some arithmetic content +% - [ReifiedOutM] is a reified version of [Out] +% as a [BFormula MFormula Tauto.isProp] % - [ReifiedOut] is a reified version of [Out] % as a [BFormula (Formula Q) Tauto.isProp] -% - [VarMap] is a variable map, that is a list of terms of type [F]. -pred quote.hyps i:rf, i:list prop, i:term, i:term, o:term, o:term, o:list term. -quote.hyps F [decl _ _ H|Ctx] Type TypeF Type'' TypeF'' VM :- - quote F H H' VM, not (H' = {{ X _ _ }}), !, - quote.hyps F Ctx Type TypeF Type' TypeF' VM, +% - [VM] is a variable map, that is a list of terms of type [F]. +pred quote.hyps i:rf, i:list prop, i:term, i:term, i:term, + o:term, o:term, o:term, o:list term. +quote.hyps F [decl _ _ H|Ctx] Type TypeFM TypeF Type'' TypeFM'' TypeF'' VM :- + quote F H HM' H' VM, not (H' = {{ X _ _ }}), !, + quote.hyps F Ctx Type TypeFM TypeF Type' TypeFM' TypeF' VM, Type'' = {{ lp:H -> lp:Type' }}, + TypeFM'' = {{ IMPL lp:HM' None lp:TypeFM' }}, TypeF'' = {{ IMPL lp:H' None lp:TypeF' }}. -quote.hyps F [decl _ _ _|Ctx] Type TypeF Type' TypeF' VM :- !, - quote.hyps F Ctx Type TypeF Type' TypeF' VM. -quote.hyps F [def _ _ _ _|Ctx] Type TypeF Type' TypeF' VM :- !, - quote.hyps F Ctx Type TypeF Type' TypeF' VM. -quote.hyps _ [] Type TypeF Type TypeF _. +quote.hyps F [decl _ _ _|Ctx] Type TypeFM TypeF Type' TypeFM' TypeF' VM :- !, + quote.hyps F Ctx Type TypeFM TypeF Type' TypeFM' TypeF' VM. +quote.hyps F [def _ _ _ _|Ctx] Type TypeFM TypeF Type' TypeFM' TypeF' VM :- !, + quote.hyps F Ctx Type TypeFM TypeF Type' TypeFM' TypeF' VM. +quote.hyps _ [] Type TypeFM TypeF Type TypeFM TypeF _. % [exfalso_if_not_prop In Out Bool] changes [In] to [False] % when [In] is not a [Prop] (and then set [Bool] to [true]) @@ -336,11 +414,12 @@ exfalso_if_not_prop _ {{ False }} {{ true }}. % that are the names of the Ltac1 tactic to call respactively % in the [realFieldType] and [realDomainType] case and a third argument [N], % passed unchanged as first argument to the previous tactic. -% The tactics [TacF] or [TacR] will receive five arguments: +% The tactics [TacF] or [TacR] will receive six arguments: % - [N] above % - [Efalso] a term of type [bool] indicating if the goal was changed to [False] % - [Type''] a term of type [Prop], an implication with the goal % and selected hypotheses +% - [TypeFM'] the reified [Type''] as a [BFormula MFormula Tauto.isProp] % - [TypeF'] the reified [Type''] as a [BFormula (Formula Q) Tauto.isProp] % - [VM''] a variable map, giving the interpretation to variables in [TypeF'] % it is of type [VarMap.t F] where [F] is the carrier for the detected @@ -349,8 +428,12 @@ solve (goal Ctx _Trigger Type _Proof [str TacF, str TacR, N] as G) GL :- exfalso_if_not_prop Type Type' Efalso, std.rev Ctx Ctx', !, rfstr Ctx' Type' F, !, - quote F Type' TypeF VM, !, - quote.hyps F Ctx' Type' TypeF Type'' TypeF' VM, !, + quote F Type' TypeFM TypeF VM, !, + quote.hyps F Ctx' Type' TypeFM TypeF Type'' TypeFM' TypeF' VM, !, + rf->numDomain F NDF, + std.assert-ok! + (coq.typecheck TypeFM' {{ BFormula (@Internals.MFormula lp:NDF) isProp }}) + "The reification produced an ill-typed result, this is a bug.", std.assert-ok! (coq.typecheck TypeF' {{ BFormula (Formula Q) isProp }}) "The reification produced an ill-typed result, this is a bug.", @@ -360,5 +443,6 @@ solve (goal Ctx _Trigger Type _Proof [str TacF, str TacR, N] as G) GL :- {{ VarMap.t lp:FS }} VM'', (if (F = field _) (Tac = TacF) (Tac = TacR)), - (coq.ltac.call Tac [N, trm Efalso, trm Type'', trm TypeF', trm VM''] G GL; + (coq.ltac.call + Tac [N, trm Efalso, trm Type'', trm TypeFM', trm TypeF', trm VM''] G GL; coq.ltac.fail 0). diff --git a/theories/lra.v b/theories/lra.v index 8d54fd3..c8f5c9d 100644 --- a/theories/lra.v +++ b/theories/lra.v @@ -15,6 +15,163 @@ Local Open Scope ring_scope. Module Internals. +Section MExpr. + +Implicit Types (R : ringType) (U : unitRingType) (F : fieldType). + +Inductive MExpr : ringType -> Type := + | MEX R : R -> MExpr R + | MEint R : Z -> MExpr R + | MErat F : Q -> MExpr F + | MEadd R : MExpr R -> MExpr R -> MExpr R + | MEmul R : MExpr R -> MExpr R -> MExpr R + | MEopp R : MExpr R -> MExpr R + | MEpow R : MExpr R -> N -> MExpr R + | MEmorph R R' : {rmorphism R -> R'} -> MExpr R -> MExpr R'. + +Definition pos_to_nat' p := + if (p <=? 5000)%positive then Pos.to_nat p + else Init.Nat.of_num_uint (Pos.to_num_uint p). + +Definition int_of_Z' n := + match n with + | Z0 => 0%Z + | Z.pos p => pos_to_nat' p + | Z.neg p => Negz (pos_to_nat' p).-1 + end. + +Definition Z2R {R} (x : Z) : R := (int_of_Z' x)%:~R. + +Definition Q2F {U} (x : Q) : U := + match x with + | Qmake n 1 => (int_of_Z' n)%:~R + | Qmake 1 d => GRing.inv (int_of_Z' (Zpos d))%:~R + | Qmake n d => (int_of_Z' n)%:~R / (nat_of_pos d)%:R + end. + +Fixpoint Meval_expr R (e : MExpr R) : R := + match e with + | MEX _ x => x + | MEint _ c => Z2R c + | MErat _ c => Q2F c + | MEadd _ e1 e2 => Meval_expr e1 + Meval_expr e2 + | MEmul _ e1 e2 => Meval_expr e1 * Meval_expr e2 + | MEopp _ e => - Meval_expr e + | MEpow _ e n => (Meval_expr e) ^+ (N.to_nat n) + | MEmorph _ _ f e => f (Meval_expr e) + end. + +Fixpoint Mnorm_expr R U (f : {rmorphism R -> U}) (e : MExpr R) : U := + match e in MExpr R return {rmorphism R -> U} -> U with + | MEX _ x => fun f => f x + | MEint _ c => fun=> Z2R c + | MErat _ c => fun=> Q2F c + | MEadd _ e1 e2 => fun f => Mnorm_expr f e1 + Mnorm_expr f e2 + | MEmul _ e1 e2 => fun f => Mnorm_expr f e1 * Mnorm_expr f e2 + | MEopp _ e => fun f => - Mnorm_expr f e + | MEpow _ e n => fun f => (Mnorm_expr f e) ^+ (N.to_nat n) + | MEmorph _ _ g e => fun f => Mnorm_expr [rmorphism of f \o g] e + end f. + +Definition Q2F' {U} (x : Q) : U := + (int_of_Z (Qnum x))%:~R / (nat_of_pos (Qden x))%:R. + +Lemma pos_to_nat_pos_to_nat' p : Pos.to_nat p = pos_to_nat' p. +Proof. +rewrite /pos_to_nat'; case: ifP => //= _. +rewrite -positive_N_nat -DecimalPos.Unsigned.of_to. +rewrite DecimalPos.Unsigned.of_uint_alt DecimalNat.Unsigned.of_uint_alt. +by elim: Decimal.rev => // u IHu; + rewrite /DecimalPos.Unsigned.of_lu -/(DecimalPos.Unsigned.of_lu u); + rewrite ?Nnat.N2Nat.inj_add Nnat.N2Nat.inj_mul IHu. +Qed. + +Lemma int_of_Z_int_of_Z' n : int_of_Z n = int_of_Z' n. +Proof. by case: n => //= p; rewrite pos_to_nat_pos_to_nat'. Qed. + +Lemma Q2F_Q2F' {U} x : Q2F x = Q2F' x :> U. +Proof. +rewrite /Q2F/Q2F'. +by case: x => -[|n|n] [p|p|] //; rewrite -int_of_Z_int_of_Z'// ?divr1//; + case: n; rewrite // -int_of_Z_int_of_Z' mul1r; + rewrite zify_ssreflect.SsreflectZifyInstances.nat_of_posE. +Qed. + +Lemma Mnorm_expr_correct U (e : MExpr U) : + Meval_expr e = Mnorm_expr [rmorphism of idfun] e. +Proof. +suff: forall R (e : MExpr R) (f : {rmorphism R -> U}), + f (Meval_expr e) = Mnorm_expr f e. + by move=> /(_ _ e [rmorphism of idfun]). +move=> R {}e. +elim: e => {}R. +- by []. +- by move=> c f; rewrite rmorph_int. +- by move=> c f; rewrite /= !Q2F_Q2F' rmorphM rmorph_int fmorphV rmorph_nat. +- by move=> e1 IH1 e2 IH2 f; rewrite rmorphD IH1 IH2. +- by move=> e1 IH1 e2 IH2 f; rewrite rmorphM IH1 IH2. +- by move=> e IH f; rewrite /= rmorphN IH. +- by move=> e IH n f; rewrite /= rmorphX IH. +- by move=> R' g e IH f; apply: (IH [rmorphism of f \o g]). +Qed. + +End MExpr. + +Section MFormula. + +Context {R : numDomainType}. + +Record MFormula := { Mlhs : MExpr R; Mop : Op2; Mrhs : MExpr R }. + +Definition Reval_pop2 (o : Op2) : R -> R -> Prop := + match o with + | OpEq => eq + | OpNEq => fun x y => ~ x = y + | OpLe => fun x y => x <= y + | OpGe => fun x y => x >= y + | OpLt => fun x y => x < y + | OpGt => fun x y => x > y + end. + +Definition Reval_bop2 (o : Op2) : R -> R -> bool := + match o with + | OpEq => fun x y => x == y + | OpNEq => fun x y => x != y + | OpLe => fun x y => x <= y + | OpGe => fun x y => x >= y + | OpLt => fun x y => x < y + | OpGt => fun x y => x > y + end. + +Definition Reval_op2 (k : Tauto.kind) : Op2 -> R -> R -> Tauto.rtyp k := + match k with isProp => Reval_pop2 | isBool => Reval_bop2 end. + +Definition Meval_formula (k : Tauto.kind) (ff : MFormula) := + let (lhs,o,rhs) := ff in Reval_op2 k o (Meval_expr lhs) (Meval_expr rhs). + +Definition Mnorm_formula (k : Tauto.kind) (ff : MFormula) := + let norm := Mnorm_expr [rmorphism of idfun] in + let (lhs,o,rhs) := ff in Reval_op2 k o (norm lhs) (norm rhs). + +Lemma Mnorm_formula_correct k (ff : MFormula) : + Meval_formula k ff = Mnorm_formula k ff. +Proof. by case: ff => l o r /=; rewrite !Mnorm_expr_correct. Qed. + +Lemma Mnorm_bf_correct k (ff : BFormula MFormula k) : + eval_bf Meval_formula ff = eval_bf Mnorm_formula ff. +Proof. +elim: ff => // {k}. +- by move=> k ff ?; exact: Mnorm_formula_correct. +- by move=> k ff1 IH1 ff2 IH2; congr eAND. +- by move=> k ff1 IH1 ff2 IH2; congr eOR. +- by move=> k ff IH; congr eNOT. +- by move=> k ff1 IH1 o ff2 IH2; congr eIMPL. +- by move=> k ff1 IH1 ff2 IH2; congr eIFF. +- by move=> ff1 IH1 ff2 IH2; congr eq. +Qed. + +End MFormula. + (* Define [Reval_formula] the semantics of [BFormula (Formula Z) Tauto.isProp] as arithmetic expressions on some [realDomainType]. Then prove [RTautoChecker_sound] stating that [ZTautoChecker f w = true] @@ -50,51 +207,25 @@ apply: mk_SOR_theory. - by apply/eqP; rewrite eq_sym oner_neq0. Qed. -Definition pos_to_nat' p := - if (p <=? 5000)%positive then Pos.to_nat p - else Init.Nat.of_num_uint (Pos.to_num_uint p). - -Lemma pos_to_nat_pos_to_nat' p : Pos.to_nat p = pos_to_nat' p. -Proof. -rewrite /pos_to_nat'; case: ifP => //= _. -rewrite -positive_N_nat -DecimalPos.Unsigned.of_to. -rewrite DecimalPos.Unsigned.of_uint_alt DecimalNat.Unsigned.of_uint_alt. -by elim: Decimal.rev => // u IHu; - rewrite /DecimalPos.Unsigned.of_lu -/(DecimalPos.Unsigned.of_lu u); - rewrite ?Nnat.N2Nat.inj_add Nnat.N2Nat.inj_mul IHu. -Qed. - -Definition int_of_Z' n := - match n with - | Z0 => 0%Z - | Z.pos p => pos_to_nat' p - | Z.neg p => Negz (pos_to_nat' p).-1 - end. - -Lemma int_of_Z_int_of_Z' n : int_of_Z n = int_of_Z' n. -Proof. by case: n => //= p; rewrite pos_to_nat_pos_to_nat'. Qed. - -Definition Z2R (x : Z) : R := (int_of_Z' x)%:~R. - Lemma Pos_to_nat_gt0 p : 0 < (Pos.to_nat p)%:R :> R. Proof. rewrite ltr0n; exact/ssrnat.ltP/Pos2Nat.is_pos. Qed. Lemma Pos_to_nat_neq0 p : (Pos.to_nat p)%:R != 0 :> R. Proof. by rewrite pnatr_eq0 -lt0n; apply/ssrnat.ltP/Pos2Nat.is_pos. Qed. -Lemma Z2R_add x y : Z2R (x + y) = Z2R x + Z2R y. +Lemma Z2R_add x y : Z2R (x + y) = Z2R x + Z2R y :> R. Proof. by rewrite /Z2R -!int_of_Z_int_of_Z' !rmorphD/=. Qed. -Lemma Z2R_opp x : Z2R (- x) = - Z2R x. +Lemma Z2R_opp x : Z2R (- x) = - Z2R x :> R. Proof. by rewrite /Z2R -!int_of_Z_int_of_Z' !rmorphN. Qed. -Lemma Z2R_sub x y : Z2R (x - y) = Z2R x - Z2R y. +Lemma Z2R_sub x y : Z2R (x - y) = Z2R x - Z2R y :> R. Proof. by rewrite Z2R_add Z2R_opp. Qed. -Lemma Z2R_mul x y : Z2R (x * y) = Z2R x * Z2R y. +Lemma Z2R_mul x y : Z2R (x * y) = Z2R x * Z2R y :> R. Proof. by rewrite /Z2R -!int_of_Z_int_of_Z' !rmorphM. Qed. -Lemma Z2R_eq x y : Z.eqb x y = (Z2R x == Z2R y). +Lemma Z2R_eq x y : Z.eqb x y = (Z2R x == Z2R y :> R). Proof. rewrite /Z2R -!int_of_Z_int_of_Z' eqr_int. apply/idP/idP; first by move=> /Z.eqb_spec ->. @@ -110,7 +241,7 @@ case: x y => [|x|x] [|y|y] //. by apply/ssrnat.leP/Peano.le_pred; rewrite -Pos2Nat.inj_le. Qed. -Lemma Z2R_le x y : Z.leb x y = true -> Z2R x <= Z2R y. +Lemma Z2R_le x y : Z.leb x y = true -> Z2R x <= Z2R y :> R. Proof. rewrite /Z2R -!int_of_Z_int_of_Z' ler_int => /Z.leb_le; exact: le_int_of_Z. Qed. @@ -148,29 +279,6 @@ Qed. Definition Reval_expr := eval_pexpr +%R *%R (fun x y => x - y) -%R Z2R N.to_nat (@GRing.exp R). -Definition Reval_pop2 (o : Op2) : R -> R -> Prop := - match o with - | OpEq => eq - | OpNEq => fun x y => ~ x = y - | OpLe => fun x y => x <= y - | OpGe => fun x y => x >= y - | OpLt => fun x y => x < y - | OpGt => fun x y => x > y - end. - -Definition Reval_bop2 (o : Op2) : R -> R -> bool := - match o with - | OpEq => fun x y => x == y - | OpNEq => fun x y => x != y - | OpLe => fun x y => x <= y - | OpGe => fun x y => x >= y - | OpLt => fun x y => x < y - | OpGt => fun x y => x > y - end. - -Definition Reval_op2 (k : Tauto.kind) : Op2 -> R -> R -> Tauto.rtyp k := - match k with isProp => Reval_pop2 | isBool => Reval_bop2 end. - Definition Reval_formula (e : PolEnv R) (k : Tauto.kind) (ff : Formula Z) := let (lhs,o,rhs) := ff in Reval_op2 k o (Reval_expr e lhs) (Reval_expr e rhs). @@ -188,7 +296,7 @@ Lemma Reval_formula_compat env b f : Proof. by case: f => lhs op rhs; case: b => //=; rewrite pop2_bop2. Qed. Definition Reval_nformula := - eval_nformula 0 +%R *%R eq (fun x y => x <= y) (fun x y => x < y) Z2R. + eval_nformula 0 +%R *%R eq (fun x y => x <= y) (fun x y => x < y) (@Z2R R). Definition ZTautoChecker (f : BFormula (Formula Z) Tauto.isProp) (w: list (Psatz Z)) : bool := @@ -229,31 +337,13 @@ Section RealField. Variable F : realFieldType. -Definition Q2F (x : Q) : F := - match x with - | Qmake n 1 => (int_of_Z' n)%:~R - | Qmake 1 d => GRing.inv (int_of_Z' (Zpos d))%:~R - | Qmake n d => (int_of_Z' n)%:~R / (nat_of_pos d)%:R - end. - -Definition Q2F' (x : Q) : F := - (int_of_Z (Qnum x))%:~R / (nat_of_pos (Qden x))%:R. - -Lemma Q2F_Q2F' x : Q2F x = Q2F' x. -Proof. -rewrite /Q2F/Q2F'. -by case: x => -[|n|n] [p|p|] //; rewrite -int_of_Z_int_of_Z'// ?divr1//; - case: n; rewrite // -int_of_Z_int_of_Z' mul1r; - rewrite zify_ssreflect.SsreflectZifyInstances.nat_of_posE. -Qed. - -Lemma Q2F0 : Q2F 0 = 0. +Lemma Q2F0 : Q2F 0 = 0 :> F. Proof. by rewrite Q2F_Q2F' /Q2F'/= mul0r. Qed. -Lemma Q2F1 : Q2F 1 = 1. +Lemma Q2F1 : Q2F 1 = 1 :> F. Proof. by rewrite Q2F_Q2F' /Q2F'/= Pos2Nat.inj_1 divrr// unitr1. Qed. -Lemma Q2F_add x y : Q2F (x + y) = Q2F x + Q2F y. +Lemma Q2F_add x y : Q2F (x + y) = Q2F x + Q2F y :> F. Proof. rewrite !Q2F_Q2F' /Q2F'/= rmorphD/= !rmorphM/= nat_of_mul_pos intrD. rewrite !intrM natrM mulrDl [(int_of_Z (Qnum y))%:~R * _]mulrC -!mulf_div. @@ -261,18 +351,18 @@ rewrite !zify_ssreflect.SsreflectZifyInstances.nat_of_posE -!pmulrn. by rewrite !divff ?Pos_to_nat_neq0// mulr1 mul1r. Qed. -Lemma Q2F_opp x : Q2F (- x) = - Q2F x. +Lemma Q2F_opp x : Q2F (- x) = - Q2F x :> F. Proof. by rewrite !Q2F_Q2F' /Q2F'/= rmorphN/= mulrNz mulNr. Qed. -Lemma Q2F_sub x y : Q2F (x - y) = Q2F x - Q2F y. +Lemma Q2F_sub x y : Q2F (x - y) = Q2F x - Q2F y :> F. Proof. by rewrite Q2F_add Q2F_opp. Qed. -Lemma Q2F_mul x y : Q2F (x * y) = Q2F x * Q2F y. +Lemma Q2F_mul x y : Q2F (x * y) = Q2F x * Q2F y :> F. Proof. by rewrite !Q2F_Q2F' /Q2F'/= rmorphM/= nat_of_mul_pos intrM natrM mulf_div. Qed. -Lemma Q2F_eq x y : Qeq_bool x y = (Q2F x == Q2F y). +Lemma Q2F_eq x y : Qeq_bool x y = (Q2F x == Q2F y :> F). Proof. rewrite !Q2F_Q2F' /Q2F'. rewrite !zify_ssreflect.SsreflectZifyInstances.nat_of_posE. @@ -283,7 +373,7 @@ apply/idP/idP. by rewrite /Qeq -[LHS]int_of_ZK -[RHS]int_of_ZK rmorphM/= eq !rmorphM. Qed. -Lemma Q2F_le x y : Qle_bool x y = true -> Q2F x <= Q2F y. +Lemma Q2F_le x y : Qle_bool x y = true -> Q2F x <= Q2F y :> F. Proof. rewrite !Q2F_Q2F' /Q2F' Qle_bool_iff => /le_int_of_Z; rewrite !rmorphM/= => le. rewrite !zify_ssreflect.SsreflectZifyInstances.nat_of_posE. @@ -332,7 +422,7 @@ Lemma Feval_formula_compat env b f : Proof. by case: f => lhs op rhs; case: b => //=; rewrite pop2_bop2. Qed. Definition Feval_nformula := - eval_nformula 0 +%R *%R eq (fun x y => x <= y) (fun x y => x < y) Q2F. + eval_nformula 0 +%R *%R eq (fun x y => x <= y) (fun x y => x < y) (@Q2F F). Lemma FTautoChecker_sound f w : QTautoChecker f w = true -> forall env, eval_bf (Feval_formula env) f. @@ -437,17 +527,21 @@ End Internals. (* Main tactics, called from the elpi parser (c.f., lra.elpi) *) -Ltac tacF tac efalso hyps_goal ff varmap := +Ltac tacF tac efalso hyps_goal rff ff varmap := match efalso with true => exfalso | _ => idtac end; (suff: hyps_goal by exact); + let irff := fresh "__rff" in let iff := fresh "__ff" in let ivarmap := fresh "__varmap" in let iwit := fresh "__wit" in let iprf := fresh "__prf" in + pose (irff := rff); pose (iff := ff); pose (ivarmap := varmap); tac iwit ff; pose (iprf := erefl true <: QTautoChecker iff iwit = true); + change (eval_bf Internals.Meval_formula irff); + rewrite Internals.Mnorm_bf_correct; change (eval_bf (Internals.Feval_formula (VarMap.find 0 ivarmap)) iff); exact (Internals.FTautoChecker_sound iprf (VarMap.find 0 ivarmap)). Ltac lraF n := let wlra_Q w f := wlra_Q w f in tacF wlra_Q. @@ -456,20 +550,24 @@ Ltac psatzF n := let sos_or_psatzn w f := wsos_Q w f || wpsatz_Q n w f in tacF sos_or_psatzn. -Ltac tacR tac efalso hyps_goal ff varmap := +Ltac tacR tac efalso hyps_goal rff ff varmap := match efalso with true => exfalso | _ => idtac end; (suff: hyps_goal by exact); + let irff := fresh "__rff" in let iff := fresh "__ff" in let ivarmap := fresh "__varmap" in let iwit := fresh "__wit" in let iprf := fresh "__prf" in match eval vm_compute in (Internals.BFormula_Q2Z ff) with | Some ?f => + pose (irff := rff); pose (iff := f); pose (ivarmap := varmap); tac iwit ff; let tr := Internals.seq_Psatz_Q2Z in pose (iprf := erefl true <: Internals.ZTautoChecker iff (tr iwit) = true); + change (eval_bf Internals.Meval_formula irff); + rewrite Internals.Mnorm_bf_correct; change (eval_bf (Internals.Reval_formula (VarMap.find 0 ivarmap)) iff); exact (Internals.RTautoChecker_sound iprf (VarMap.find 0 ivarmap)) | _ => fail (* should never happen, the parser only parses int constants *)