From db77cbf00b7174a57a71b148997df84047ac1ba5 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Wed, 19 Jun 2024 10:51:35 +0200 Subject: [PATCH 1/6] chore: prove `Rat` core lemmas --- Smt/Int.lean | 9 + Smt/Rat.lean | 8 + Smt/Reconstruct/Int.lean | 428 +++++++++++++++++++++++++++++ Smt/Reconstruct/Int/Lemmas.lean | 141 ++++------ Smt/Reconstruct/Int/Polynorm.lean | 232 ++++++++++++++++ Smt/Reconstruct/Int/Rewrites.lean | 7 +- Smt/Reconstruct/Rat.lean | 430 ++++++++++++++++++++++++++++++ Smt/Reconstruct/Rat/Core.lean | 177 ++++++++++++ Smt/Reconstruct/Rat/Lemmas.lean | 210 +++++++++++++++ Smt/Reconstruct/Rat/Polynorm.lean | 279 +++++++++++++++++++ Smt/Reconstruct/Rat/Rewrites.lean | 83 ++++++ 11 files changed, 1907 insertions(+), 97 deletions(-) create mode 100644 Smt/Int.lean create mode 100644 Smt/Rat.lean create mode 100644 Smt/Reconstruct/Int.lean create mode 100644 Smt/Reconstruct/Int/Polynorm.lean create mode 100644 Smt/Reconstruct/Rat.lean create mode 100644 Smt/Reconstruct/Rat/Core.lean create mode 100644 Smt/Reconstruct/Rat/Lemmas.lean create mode 100644 Smt/Reconstruct/Rat/Polynorm.lean create mode 100644 Smt/Reconstruct/Rat/Rewrites.lean diff --git a/Smt/Int.lean b/Smt/Int.lean new file mode 100644 index 00000000..e1ace45e --- /dev/null +++ b/Smt/Int.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct.Int +import Smt.Translate.Int diff --git a/Smt/Rat.lean b/Smt/Rat.lean new file mode 100644 index 00000000..f9e2503e --- /dev/null +++ b/Smt/Rat.lean @@ -0,0 +1,8 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct.Rat diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean new file mode 100644 index 00000000..89e8d742 --- /dev/null +++ b/Smt/Reconstruct/Int.lean @@ -0,0 +1,428 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct +import Smt.Reconstruct.Builtin.Lemmas +import Smt.Reconstruct.Int.Lemmas +import Smt.Reconstruct.Int.Polynorm +import Smt.Reconstruct.Int.Rewrites +import Smt.Reconstruct.Rewrite + +namespace Smt.Reconstruct.Int + +open Lean +open Qq + +@[smt_sort_reconstruct] def reconstructIntSort : SortReconstructor := fun s => do match s.getKind with + | .INTEGER_SORT => return q(Int) + | _ => return none + +@[smt_term_reconstruct] def reconstructInt : TermReconstructor := fun t => do match t.getKind with + | .SKOLEM => match t.getSkolemId with + | .INT_DIV_BY_ZERO => return q(fun (x : Int) => x / 0) + | .MOD_BY_ZERO => return q(fun (x : Int) => x % 0) + | _ => return none + | .CONST_INTEGER => + let x : Int := t.getIntegerValue + let x' : Q(Nat) := mkRawNatLit x.natAbs + if x ≥ 0 then + return q(OfNat.ofNat $x' : Int) + else + return q(-(OfNat.ofNat $x' : Int)) + | .NEG => + if !t.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + return q(-$x) + | .SUB => + if !t.getSort.isInteger then return none + leftAssocOp q(@HSub.hSub Int Int Int _) t + | .ADD => + if !t.getSort.isInteger then return none + leftAssocOp q(@HAdd.hAdd Int Int Int _) t + | .MULT => + if !t.getSort.isInteger then return none + leftAssocOp q(@HMul.hMul Int Int Int _) t + | .INTS_DIVISION => + leftAssocOp q(@HDiv.hDiv Int Int Int _) t + | .INTS_DIVISION_TOTAL => + leftAssocOp q(@HDiv.hDiv Int Int Int _) t + | .INTS_MODULUS => + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x % $y) + | .INTS_MODULUS_TOTAL => + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x % $y) + | .ABS => + if !t.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + return q(if $x < 0 then -$x else $x) + | .LEQ => + if !t[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x ≤ $y) + | .LT => + if !t[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x < $y) + | .GEQ => + if !t[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x ≥ $y) + | .GT => + if !t[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x > $y) + | _ => return none +where + leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do + let mut curr ← reconstructTerm t[0]! + for i in [1:t.getNumChildren] do + curr := mkApp2 op curr (← reconstructTerm t[i]!) + return curr + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match pf.getRewriteRule with + | .ARITH_PLUS_ZERO => + if !pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_zero) args) + | .ARITH_MUL_ONE => + if !pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mul_one) args) + | .ARITH_MUL_ZERO => + if !pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mul_zero) args) + | .ARITH_INT_DIV_TOTAL => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]! + addThm q($t / $s = $t / $s) q(@Rewrite.int_div_total $t $s $h) + | .ARITH_INT_DIV_TOTAL_ONE => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q($t / 1 = $t) q(@Rewrite.int_div_total_one $t) + | .ARITH_INT_DIV_TOTAL_ZERO => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q($t / 0 = 0) q(@Rewrite.int_div_total_zero $t) + | .ARITH_INT_MOD_TOTAL => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]! + addThm q($t % $s = $t % $s) q(@Rewrite.int_mod_total $t $s $h) + | .ARITH_INT_MOD_TOTAL_ONE => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q($t % 1 = 0) q(@Rewrite.int_mod_total_one $t) + | .ARITH_INT_MOD_TOTAL_ZERO => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q($t % 0 = $t) q(@Rewrite.int_mod_total_zero $t) + | .ARITH_NEG_NEG_ONE => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(-1 * (-1 * $t) = $t) q(@Rewrite.neg_neg_one $t) + | .ARITH_ELIM_UMINUS => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(-$t = -1 * $t) q(@Rewrite.elim_uminus $t) + | .ARITH_ELIM_MINUS => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q($t - $s = $t + -1 * $s) q(@Rewrite.elim_minus $t $s) + | .ARITH_ELIM_GT => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t > $s) = ¬($t ≤ $s)) q(@Rewrite.elim_gt $t $s) + | .ARITH_ELIM_LT => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t < $s) = ¬($t ≥ $s)) q(@Rewrite.elim_lt $t $s) + -- | .ARITH_ELIM_INT_GT => + -- let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + -- let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + -- addThm q(($t > $s) = ($t ≥ $s + 1)) q(@Rewrite.elim_int_gt $t $s) + -- | .ARITH_ELIM_INT_LT => + -- let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + -- let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + -- addThm q(($t < $s) = ($s ≥ $t + 1)) q(@Rewrite.elim_int_lt $t $s) + | .ARITH_ELIM_LEQ => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≤ $s) = ($s ≥ $t)) q(@Rewrite.elim_leq $t $s) + | .ARITH_LEQ_NORM => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≤ $s) = ¬($t ≥ $s + 1)) q(@Rewrite.leq_norm $t $s) + | .ARITH_GEQ_TIGHTEN => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q((¬($t ≥ $s)) = ($s ≥ $t + 1)) q(@Rewrite.geq_tighten $t $s) + | .ARITH_GEQ_NORM1 => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = ($t - $s ≥ 0)) q(@Rewrite.geq_norm1 $t $s) + | .ARITH_GEQ_NORM2 => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = (-$t ≤ -$s)) q(@Rewrite.geq_norm2 $t $s) + | .ARITH_REFL_LEQ => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≤ $t) = True) q(@Rewrite.refl_leq $t) + | .ARITH_REFL_LT => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(($t < $t) = False) q(@Rewrite.refl_lt $t) + | .ARITH_REFL_GEQ => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≥ $t) = True) q(@Rewrite.refl_geq $t) + | .ARITH_REFL_GT => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(($t > $t) = False) q(@Rewrite.refl_gt $t) + | .ARITH_PLUS_FLATTEN => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_flatten) args) + | .ARITH_MULT_FLATTEN => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mult_flatten) args) + | .ARITH_MULT_DIST => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mult_dist) args) + | .ARITH_PLUS_CANCEL1 => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.plus_cancel1) args) + | .ARITH_PLUS_CANCEL2 => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_cancel2) args) + | .ARITH_ABS_ELIM => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(ite ($t < 0) (-$t) $t = ite ($t < 0) (-$t) $t) q(@Rewrite.abs_elim $t) + | _ => return none +where + reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do + let mut args' := #[] + for arg in args do + let mut arg' := #[] + for subarg in arg do + arg' := arg'.push (← reconstructTerm subarg) + args' := args'.push arg' + return args' + +def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let f := fun (ks, ls, rs, hs) p => do + let l : Q(Int) ← reconstructTerm p.getResult[0]! + let r : Q(Int) ← reconstructTerm p.getResult[1]! + let lsl := q($ls + $l) + let rsr := q($rs + $r) + let k := p.getResult.getKind + if ks == .LT && k == .LT then + let hs : Q($ls < $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₁ $hs $h)) + else if ks == .LT && k == .LEQ then + let hs : Q($ls < $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₂ $hs $h)) + else if ks == .LT && k == .EQUAL then + let hs : Q($ls < $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₃ $hs $h)) + else if ks == .LEQ && k == .LT then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₄ $hs $h)) + else if ks == .LEQ && k == .LEQ then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Int.sum_ub₅ $hs $h)) + else if ks == .LEQ && k == .EQUAL then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Int.sum_ub₆ $hs $h)) + else if ks == .EQUAL && k == .LT then + let hs : Q($ls = $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₇ $hs $h)) + else if ks == .EQUAL && k == .LEQ then + let hs : Q($ls = $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Int.sum_ub₈ $hs $h)) + else if ks == .EQUAL && k == .EQUAL then + let hs : Q($ls = $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.EQUAL, lsl, rsr, q(Int.sum_ub₉ $hs $h)) + else + throwError "[sum_ub]: invalid kinds: {ks}, {p.getResult.getKind}" + let k := pf.getChildren[0]!.getResult.getKind + let ls : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let rs : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let hs ← reconstructProof pf.getChildren[0]! + let (_, ls, rs, hs) ← pf.getChildren[1:].foldlM f (k, ls, rs, hs) + addThm q($ls < $rs) hs + +def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let ts := pf.getResult[0]!.getChildren + let mut hs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + let mut map : HashMap cvc5.Term Nat := {} + for h : i in [0:ts.size] do + let t := ts[i]'(h.right) + let p : Q(Prop) ← reconstructTerm t + hs := hs.push (Name.num `a i, fun _ => return p) + map := map.insert (if t.getKind == .NOT then t[0]![0]! else t[0]!) i + let t := pf.getResult[1]! + let vs := if t[0]!.getKind == .CONST_INTEGER then t[1]!.getChildren else t[0]!.getChildren + let f t ps := do + let p : Q(Prop) ← reconstructTerm t + return q($p :: $ps) + let ps : Q(List Prop) ← ts.foldrM f q([]) + let q : Q(Prop) ← reconstructTerm t + let h : Q(impliesN $ps $q) ← Meta.withLocalDeclsD hs fun hs => do + let h : Q($q) ← if ts[map.find! vs[0]!]!.getKind == .NOT then + let a : Q(Int) ← reconstructTerm vs[0]! + let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]! + go vs ts hs map .GT q($a * $a) q(Int.mul_sign₀ $ha) 2 + else + let a : Q(Int) ← reconstructTerm vs[0]! + go vs ts hs map ts[map.find! vs[0]!]!.getKind a hs[map.find! vs[0]!]! 1 + Meta.mkLambdaFVars hs h + addThm q(andN $ps → $q) q(Builtin.scopes $h) +where + go vs ts hs map ka (a : Q(Int)) (ha : Expr) i : ReconstructM Expr := do + if hi : i < vs.size then + let b : Q(Int) ← reconstructTerm vs[i] + let k := ts[map.find! vs[i]]!.getKind + if ka == .LT && k == .LT then + let ha : Q($a < 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Int.mul_sign₁ $ha $hb) (i + 1) + else if ka == .LT && k == .NOT then + let ha : Q($a < 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b * $b) q(Int.mul_sign₂ $ha $hb) (i + 2) + else if ka == .LT && k == .GT then + let ha : Q($a < 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Int.mul_sign₃ $ha $hb) (i + 1) + else if ka == .GT && k == .LT then + let ha : Q($a > 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Int.mul_sign₄ $ha $hb) (i + 1) + else if ka == .GT && k == .NOT then + let ha : Q($a > 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b * $b) q(Int.mul_sign₅ $ha $hb) (i + 2) + else if ka == .GT && k == .GT then + let ha : Q($a > 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Int.mul_sign₆ $ha $hb) (i + 1) + else + throwError "[mul_sign]: invalid kinds: {ka}, {k}" + else + return ha + +@[smt_proof_reconstruct] def reconstructIntProof : ProofReconstructor := fun pf => do match pf.getRule with + | .DSL_REWRITE + | .THEORY_REWRITE => reconstructRewrite pf + | .ARITH_SUM_UB => + if !pf.getResult[0]!.getSort.isInteger then return none + reconstructSumUB pf + | .ARITH_TRICHOTOMY => + if !pf.getResult[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm pf.getResult[0]! + let c : Q(Int) ← reconstructTerm pf.getResult[1]! + let k₁ := pf.getChildren[0]!.getResult.getKind + let k₂ := pf.getChildren[1]!.getResult.getKind + if k₁ == .GEQ && k₂ == .NOT then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Int.trichotomy₁ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .GEQ then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Int.trichotomy₂ $h₁ $h₂) + else if k₁ == .GEQ && k₂ == .LEQ then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Int.trichotomy₃ $h₁ $h₂) + else if k₁ == .LEQ && k₂ == .GEQ then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Int.trichotomy₄ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .LT then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Int.trichotomy₅ $h₁ $h₂) + else if k₁ == .LT && k₂ == .NOT then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Int.trichotomy₆ $h₁ $h₂) + else + return none + | .ARITH_POLY_NORM => + if !pf.getResult[0]!.getSort.isInteger then return none + let a : Q(Int) ← reconstructTerm pf.getResult[0]! + let b : Q(Int) ← reconstructTerm pf.getResult[1]! + addTac q($a = $b) Int.polyNorm + | .ARITH_MULT_SIGN => + if !pf.getResult[1]![0]!.getSort.isInteger then return none + reconstructMulSign pf + | .ARITH_MULT_POS => + if !pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Int) ← reconstructTerm pf.getArguments[0]! + let l : Q(Int) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Int) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m > 0 ∧ $l < $r → $m * $l < $m * $r) q(@Int.mul_pos_lt $l $r $m) + | .LEQ => + addThm q($m > 0 ∧ $l ≤ $r → $m * $l ≤ $m * $r) q(@Int.mul_pos_le $l $r $m) + | .EQUAL => + addThm q($m > 0 ∧ $l = $r → $m * $l = $m * $r) q(@Int.mul_pos_eq $l $r $m) + | .GEQ => + addThm q($m > 0 ∧ $l ≥ $r → $m * $l ≥ $m * $r) q(@Int.mul_pos_ge $l $r $m) + | .GT => + addThm q($m > 0 ∧ $l > $r → $m * $l > $m * $r) q(@Int.mul_pos_gt $l $r $m) + | _ => return none + | .ARITH_MULT_NEG => + if !pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Int) ← reconstructTerm pf.getArguments[0]! + let l : Q(Int) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Int) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m < 0 ∧ $l < $r → $m * $l > $m * $r) q(@Int.mul_neg_lt $l $r $m) + | .LEQ => + addThm q($m < 0 ∧ $l ≤ $r → $m * $l ≥ $m * $r) q(@Int.mul_neg_le $l $r $m) + | .EQUAL => + addThm q($m < 0 ∧ $l = $r → $m * $l = $m * $r) q(@Int.mul_neg_eq $l $r $m) + | .GEQ => + addThm q($m < 0 ∧ $l ≥ $r → $m * $l ≤ $m * $r) q(@Int.mul_neg_ge $l $r $m) + | .GT => + addThm q($m < 0 ∧ $l > $r → $m * $l < $m * $r) q(@Int.mul_neg_gt $l $r $m) + | _ => return none + | _ => return none + +end Smt.Reconstruct.Int diff --git a/Smt/Reconstruct/Int/Lemmas.lean b/Smt/Reconstruct/Int/Lemmas.lean index 448ce906..d7e86d67 100644 --- a/Smt/Reconstruct/Int/Lemmas.lean +++ b/Smt/Reconstruct/Int/Lemmas.lean @@ -5,16 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed -/ -private theorem Nat.mod_two_ne_zero : ¬n % 2 = 0 ↔ n % 2 = 1 := by - cases Nat.mod_two_eq_zero_or_one n <;> rename_i h <;> simp [h] - -private theorem Nat.even_add : (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0) := by - cases Nat.mod_two_eq_zero_or_one m <;> rename_i h₁ <;> cases Nat.mod_two_eq_zero_or_one n <;> rename_i h₂ <;> - simp [h₁, h₂, Nat.add_mod] - -private theorem Nat.even_add_one : (n + 1) % 2 = 0 ↔ n % 2 ≠ 0 := by - simp [Nat.even_add] - private theorem Int.mul_lt_mul_left {c x y : Int} (hc : c > 0) : (c * x < c * y) = (x < y) := by apply propext constructor @@ -33,23 +23,13 @@ private theorem Int.mul_eq_zero_left {x y : Int} (hx : x ≠ 0) (hxy : x * y = 0 private def uncurry {p₁ p₂ p₃ : Prop} : (p₁ → p₂ → p₃) → (p₁ ∧ p₂) → p₃ := by intros h₁ h₂ - have ⟨ ht₁, ht₂ ⟩ := h₂ + have ⟨ht₁, ht₂⟩ := h₂ exact h₁ ht₁ ht₂ namespace Smt.Reconstruct.Int variable {a b c d : Int} -private theorem or_implies_left (hpq : p ∨ q) (hnq : ¬q) : p := by - cases hpq with - | inl hp => exact hp - | inr hq => exact False.elim (hnq hq) - -private theorem or_implies_right (hpq : p ∨ q) (hnp : ¬p) : q := by - cases hpq with - | inl hp => exact False.elim (hnp hp) - | inr hq => exact hq - theorem sum_ub₁ (h₁ : a < b) (h₂ : c < d) : a + c < b + d := by have r₁: a + c < a + d := Int.add_lt_add_left h₂ a have r₂: a + d < b + d := Int.add_lt_add_right h₁ d @@ -92,27 +72,27 @@ theorem sum_ub₉ (h₁ : a = b) (h₂ : c = d) : a + c ≤ b + d := by theorem trichotomy₁ (h₁ : a ≥ b) (h₂ : a ≠ b) : a > b := by have tr := Int.lt_trichotomy a b - exact or_implies_right (or_implies_right tr (Int.not_lt.mpr h₁)) h₂ + exact Or.resolve_left (Or.resolve_left tr (Int.not_lt.mpr h₁)) h₂ theorem trichotomy₂ (h₁ : a ≠ b) (h₂ : a ≥ b) : a > b := by have tr := Int.lt_trichotomy a b - exact or_implies_right (or_implies_right tr (Int.not_lt.mpr h₂)) h₁ + exact Or.resolve_left (Or.resolve_left tr (Int.not_lt.mpr h₂)) h₁ theorem trichotomy₃ (h₁ : a ≥ b) (h₂ : a ≤ b) : a = b := by have tr := Int.lt_trichotomy a b - exact or_implies_left (or_implies_right tr (Int.not_lt.mpr h₁)) (Int.not_lt.mpr h₂) + exact Or.resolve_right (Or.resolve_left tr (Int.not_lt.mpr h₁)) (Int.not_lt.mpr h₂) theorem trichotomy₄ (h₁ : a ≤ b) (h₂ : a ≥ b) : a = b := by have tr := Int.lt_trichotomy a b - exact or_implies_left (or_implies_right tr (Int.not_lt.mpr h₂)) (Int.not_lt.mpr h₁) + exact Or.resolve_right (Or.resolve_left tr (Int.not_lt.mpr h₂)) (Int.not_lt.mpr h₁) theorem trichotomy₅ (h₁ : a ≠ b) (h₂ : a ≤ b) : a < b := by have tr := Int.lt_trichotomy a b - exact or_implies_left (or_implies_left (or_assoc.mpr tr) (Int.not_lt.mpr h₂)) h₁ + exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (Int.not_lt.mpr h₂)) h₁ theorem trichotomy₆ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by have tr := Int.lt_trichotomy a b - exact or_implies_left (or_implies_left (or_assoc.mpr tr) (Int.not_lt.mpr h₁)) h₂ + exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (Int.not_lt.mpr h₁)) h₂ theorem lt_eq_sub_lt_zero : (a < b) = (a - b < 0) := by apply propext @@ -168,95 +148,72 @@ theorem gt_of_sub_eq {c₁ c₂ : Int} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h rw (config := { occs := .pos [1] }) [← Int.mul_zero c, gt_iff_lt, Int.mul_lt_mul_left hc] rw [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero b₁, ← this hc₁, ← this hc₂, h] -mutual - -theorem pow_neg_even {k : Nat} {z : Int} (h₁ : z < 0) (h₂ : k % 2 = 0) : z ^ k > 0 := by - cases k with - | zero => simp [Int.pow_zero] - | succ k => - have hodd := Nat.even_add_one.mp h₂ - have mulZ : z * z ^ k > z * 0 := Int.mul_lt_mul_of_neg_left (pow_neg_odd h₁ (Nat.mod_two_ne_zero.mp hodd)) h₁ - simp at mulZ - rw [Int.pow_succ, Int.mul_comm] - exact mulZ - -theorem pow_neg_odd {k : Nat} {z : Int} (h₁ : z < 0) (h₂ : k % 2 = 1) : z ^ k < 0 := by - cases k with - | zero => simp at h₂ - | succ k => - have heven : k % 2 = 0 := Classical.not_not.mp (mt Nat.even_add_one.mpr (Eq.symm h₂ ▸ nofun)) - have mulZ : z * 0 > z * z ^ k := Int.mul_lt_mul_of_neg_left (pow_neg_even h₁ heven) h₁ - simp at mulZ - rw [Int.pow_succ, Int.mul_comm] - exact mulZ - -end - -theorem pow_pos {k : Nat} {z : Int} (h : z > 0) : z ^ k > 0 := by - induction k with - | zero => simp [Int.pow_zero] - | succ k ih => - rw [Int.pow_succ] - have h₂ := Int.mul_lt_mul_of_pos_left h ih - simp at h₂ - exact h₂ - -theorem non_zero_even_pow {k : Nat} {z : Int} (h₁ : z ≠ 0) (h₂ : k % 2 = 0) : z ^ k > 0 := by - match Int.lt_trichotomy z 0 with - | Or.inl hneg => exact pow_neg_even hneg h₂ - | Or.inr (Or.inl hzero) => rw [hzero] at h₁; simp at h₁ - | Or.inr (Or.inr hpos) => exact pow_pos hpos - -theorem combine_signs₁ : a > 0 → b > 0 → b * a > 0 := by - intros h₁ h₂ - have h := Int.mul_lt_mul_of_pos_left h₁ h₂ +theorem mul_sign₁ (ha : a < 0) (hb : b < 0) : a * b > 0 := by + have h := Int.mul_lt_mul_of_neg_right ha hb simp at h exact h -theorem combine_signs₂ : a > 0 → b < 0 → b * a < 0 := by - intros h₁ h₂ - have h := Int.mul_lt_mul_of_pos_right h₂ h₁ +theorem mul_sign₃ (ha : a < 0) (hb : b > 0) : a * b < 0 := by + have h := Int.mul_lt_mul_of_pos_right ha hb simp at h exact h -theorem combine_signs₃ : a < 0 → b > 0 → b * a < 0 := by - intros h₁ h₂ - have h := Int.mul_lt_mul_of_pos_left h₁ h₂ +theorem mul_sign₄ (ha : a > 0) (hb : b < 0) : a * b < 0 := by + have h := Int.mul_lt_mul_of_pos_left hb ha simp at h exact h -theorem combine_signs₄ : a < 0 → b < 0 → b * a > 0 := by - intros h₁ h₂ - have h := Int.mul_lt_mul_of_neg_left h₁ h₂ +theorem mul_sign₆ (ha : a > 0) (hb : b > 0) : a * b > 0 := by + have h := Int.mul_lt_mul_of_pos_left hb ha simp at h exact h -theorem arith_mul_pos_lt : c > 0 ∧ a < b → c * a < c * b := - uncurry (flip Int.mul_lt_mul_of_pos_left) +theorem mul_sign₀ (ha : a ≠ 0) : a * a > 0 := + match Int.lt_trichotomy a 0 with + | .inl hn => mul_sign₁ hn hn + | .inr (.inl hz) => absurd hz ha + | .inr (.inr hp) => mul_sign₆ hp hp + +theorem mul_sign₂ (ha : a < 0) (hb : b ≠ 0) : a * b * b < 0 := + match Int.lt_trichotomy b 0 with + | .inl hn => mul_sign₄ (mul_sign₁ ha hn) hn + | .inr (.inl hz) => absurd hz hb + | .inr (.inr hp) => mul_sign₃ (mul_sign₃ ha hp) hp + +theorem mul_sign₅ (ha : a > 0) (hb : b ≠ 0) : a * b * b > 0 := + match Int.lt_trichotomy b 0 with + | .inl hn => mul_sign₁ (mul_sign₄ ha hn) hn + | .inr (.inl hz) => absurd hz hb + | .inr (.inr hp) => mul_sign₆ (mul_sign₆ ha hp) hp + +theorem mul_pos_lt (h : c > 0 ∧ a < b) : c * a < c * b := + Int.mul_lt_mul_of_pos_left h.2 h.1 -theorem arith_mul_pos_le : c > 0 ∧ a ≤ b → c * a ≤ c * b := λ h => +theorem mul_pos_le (h : c > 0 ∧ a ≤ b) : c * a ≤ c * b := Int.mul_le_mul_of_nonneg_left h.2 (Int.le_of_lt h.1) -theorem arith_mul_pos_gt : c > 0 ∧ a > b → c * a > c * b := arith_mul_pos_lt +theorem mul_pos_gt (h : c > 0 ∧ a > b) : c * a > c * b := + mul_pos_lt h -theorem arith_mul_pos_ge : c > 0 ∧ a ≥ b → c * a ≥ c * b := arith_mul_pos_le +theorem mul_pos_ge (h : c > 0 ∧ a ≥ b) : c * a ≥ c * b := + mul_pos_le h -theorem arith_mul_pos_eq : c > 0 ∧ a = b → c * a = c * b := by - intros h +theorem mul_pos_eq (h : c > 0 ∧ a = b) : c * a = c * b := by rw [h.2] -theorem arith_mul_neg_lt : c < 0 ∧ a < b → c * a > c * b := - uncurry (flip Int.mul_lt_mul_of_neg_left) +theorem mul_neg_lt (h : c < 0 ∧ a < b) : c * a > c * b := + Int.mul_lt_mul_of_neg_left h.2 h.1 -theorem arith_mul_neg_le : c < 0 ∧ a ≤ b → c * a ≥ c * b := λ h => +theorem mul_neg_le (h : c < 0 ∧ a ≤ b) : c * a ≥ c * b := Int.mul_le_mul_of_nonpos_left (Int.le_of_lt h.1) h.2 -theorem arith_mul_neg_gt : c < 0 ∧ a > b → c * a < c * b := arith_mul_neg_lt +theorem mul_neg_gt (h : c < 0 ∧ a > b) : c * a < c * b := + mul_neg_lt h -theorem arith_mul_neg_ge : c < 0 ∧ a ≥ b → c * a ≤ c * b := arith_mul_neg_le +theorem mul_neg_ge (h : c < 0 ∧ a ≥ b) : c * a ≤ c * b := + mul_neg_le h -theorem arith_mul_neg_eq : c < 0 ∧ a = b → c * a = c * b := by - intros h +theorem mul_neg_eq (h : c < 0 ∧ a = b) : c * a = c * b := by rw [h.2] end Smt.Reconstruct.Int diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean new file mode 100644 index 00000000..983cd71b --- /dev/null +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -0,0 +1,232 @@ +/- +Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Lean +import Qq + +namespace Smt.Reconstruct.Int.PolyNorm + +abbrev Var := Nat + +def Context := Var → Int + +structure Monomial where + coeff : Int + vars : List Var +deriving Inhabited, Repr + +namespace Monomial + +open Qq in +def toExpr (m : Monomial) (ppCtx : Var → Q(Int)) : Q(Int) := + if h : m.vars = [] then + toExprCoeff m.coeff + else + if m.coeff = 1 then + (m.vars.drop 1).foldl (fun acc v => q($acc * $(ppCtx v))) (ppCtx (m.vars.head h)) + else + m.vars.foldl (fun acc v => q($acc * $(ppCtx v))) (toExprCoeff m.coeff) +where + toExprCoeff (c : Int) : Q(Int) := + let l : Q(Nat) := Lean.mkRawNatLit c.natAbs + if c ≥ 0 then + q(OfNat.ofNat $l : Int) + else + q(-OfNat.ofNat $l : Int) + +def neg (m : Monomial) : Monomial := + { m with coeff := -m.coeff } + +def add (m₁ m₂ : Monomial) (_ : m₁.vars = m₂.vars) : Monomial := + { coeff := m₁.coeff + m₂.coeff, vars := m₁.vars } + +-- Invariant: monomial variables remain sorted. +def mul (m₁ m₂ : Monomial) : Monomial := + let coeff := m₁.coeff * m₂.coeff + let vars := m₁.vars.foldr insert m₂.vars + { coeff, vars } +where + insert (x : Var) : List Var → List Var + | [] => [x] + | y :: ys => if x ≤ y then x :: y :: ys else y :: insert x ys + +def denote (ctx : Context) (m : Monomial) : Int := + m.coeff * m.vars.foldl (fun acc v => acc * ctx v) 1 + +theorem denote_neg {m : Monomial} : m.neg.denote ctx = -m.denote ctx := by + simp only [neg, denote, Int.neg_mul_eq_neg_mul] + +theorem denote_mul {m₁ m₂ : Monomial} : (m₁.mul m₂).denote ctx = m₁.denote ctx * m₂.denote ctx := + sorry + +end Monomial + +abbrev Polynomial := List Monomial + +namespace Polynomial + +open Qq in +def toExpr (p : Polynomial) (ppCtx : Var → Q(Int)) : Q(Int) := + go p +where + go : Polynomial → Q(Int) + | [] => q(0) + | [m] => m.toExpr ppCtx + | m :: ms =>q($(m.toExpr ppCtx) + $(go ms)) + +def neg (p : Polynomial) : Polynomial := + p.map Monomial.neg + +-- NOTE: implementation merges monomials with same variables. +-- Invariant: monomials remain sorted. +def add (p q : Polynomial) : Polynomial := + p.foldr insert q +where + insert (m : Monomial) : Polynomial → Polynomial + | [] => [m] + | n :: ns => + if m.vars < n.vars then + m :: n :: ns + else if h : m.vars = n.vars then + let m' := m.add n h + if m'.coeff = 0 then ns else m' :: ns + else + n :: insert m ns + +def sub (p q : Polynomial) : Polynomial := + p.add q.neg + +-- Invariant: monomials remain sorted. +def mulMonomial (m : Monomial) (p : Polynomial) : Polynomial := + p.foldr (fun n acc => Polynomial.add [m.mul n] acc) [] + +-- Invariant: monomials remain sorted. +def mul (p q : Polynomial) : Polynomial := + p.foldl (fun acc m => (q.mulMonomial m).add acc) [] + +def denote (ctx : Context) (p : Polynomial) : Int := + p.foldl (fun acc m => acc + m.denote ctx) 0 + +theorem denote_neg {p : Polynomial} : p.neg.denote ctx = -p.denote ctx := + sorry + +theorem denote_add {p q : Polynomial} : (p.add q).denote ctx = p.denote ctx + q.denote ctx := + sorry + +theorem denote_sub {p q : Polynomial} : (p.sub q).denote ctx = p.denote ctx - q.denote ctx := by + simp only [sub, denote_neg, denote_add, Int.sub_eq_add_neg] + +theorem denote_mulMonomial {p : Polynomial} : (p.mulMonomial m).denote ctx = m.denote ctx * p.denote ctx := + sorry + +theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.denote ctx := + sorry + +end Polynomial + +inductive Expr where + | val (v : Int) + | var (v : Nat) + | neg (a : Expr) + | add (a b : Expr) + | mul (a b : Expr) + | sub (a b : Expr) +deriving Inhabited, Repr + +namespace Expr + +def toPolynomial : Expr → Polynomial + | val v => if v = 0 then [] else [{ coeff := v, vars := [] }] + | var v => [{ coeff := 1, vars := [v] }] + | neg a => a.toPolynomial.neg + | add a b => Polynomial.add a.toPolynomial b.toPolynomial + | sub a b => Polynomial.sub a.toPolynomial b.toPolynomial + | mul a b => Polynomial.mul a.toPolynomial b.toPolynomial + +def denote (ctx : Context) : Expr → Int + | val v => v + | var v => ctx v + | neg a => -a.denote ctx + | add a b => a.denote ctx + b.denote ctx + | sub a b => a.denote ctx - b.denote ctx + | mul a b => a.denote ctx * b.denote ctx + +theorem denote_toPolynomial {e : Expr} : e.denote ctx = e.toPolynomial.denote ctx := by + induction e with + | val v => + simp only [denote, toPolynomial] + split <;> rename_i hv + · rewrite [hv]; rfl + · simp [Polynomial.denote, Monomial.denote] + | var v => + simp [denote, toPolynomial, Polynomial.denote, Monomial.denote] + | neg a ih => + simp only [denote, toPolynomial, Polynomial.denote_neg, ih] + | add a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_add, ih₁, ih₂] + | sub a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_sub, ih₁, ih₂] + | mul a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_mul, ih₁, ih₂] + +theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : Expr} (h : e₁.toPolynomial = e₂.toPolynomial) : e₁.denote ctx = e₂.denote ctx := by + rw [denote_toPolynomial, denote_toPolynomial, h] + +end PolyNorm.Expr + +open Lean Qq + +abbrev PolyM := StateT (Array Q(Int)) MetaM + +def getIndex (e : Q(Int)) : PolyM Nat := do + let es ← get + if let some i := es.findIdx? (· == e) then + return i + else + let size := es.size + set (es.push e) + return size + +partial def toArithExpr (e : Q(Int)) : PolyM Q(PolyNorm.Expr) := do + match e with + | ~q(OfNat.ofNat $x) => pure q(.val (@OfNat.ofNat Int $x _)) + | ~q(-$x) => pure q(.neg $(← toArithExpr x)) + | ~q($x + $y) => pure q(.add $(← toArithExpr x) $(← toArithExpr y)) + | ~q($x - $y) => pure q(.sub $(← toArithExpr x) $(← toArithExpr y)) + | ~q($x * $y) => pure q(.mul $(← toArithExpr x) $(← toArithExpr y)) + | e => let v : Nat ← getIndex e; pure q(.var $v) + +def polyNorm (mv : MVarId) : MetaM Unit := do + let some (_, l, r) := (← mv.getType).eq? + | throwError "[poly_norm] expected an equality, got {← mv.getType}" + let (l, es) ← (toArithExpr l).run #[] + let (r, es) ← (toArithExpr r).run es + let is : Q(Array Int) := es.foldl (fun acc e => q(«$acc».push $e)) q(#[]) + let ctx : Q(PolyNorm.Context) := q(fun v => if h : v < «$is».size then $is[v] else 0) + let h : Q(«$l».toPolynomial = «$r».toPolynomial) := .app q(@Eq.refl.{1} PolyNorm.Polynomial) q(«$l».toPolynomial) + mv.assign q(@PolyNorm.Expr.denote_eq_from_toPolynomial_eq $ctx $l $r $h) +where + logPolynomial (e : Q(PolyNorm.Expr)) (es : Array Q(Int)) := do + let p ← unsafe Meta.evalExpr PolyNorm.Expr q(PolyNorm.Expr) e + let ppCtx := fun v => if h : v < es.size then es[v] else q(0) + logInfo m!"poly := {PolyNorm.Polynomial.toExpr p.toPolynomial ppCtx}" + +namespace Tactic + +syntax (name := polyNorm) "poly_norm" : tactic + +open Lean.Elab Tactic in +@[tactic polyNorm] def evalPolyNorm : Tactic := fun _ => + withMainContext do + let mv ← Tactic.getMainGoal + Int.polyNorm mv + replaceMainGoal [] + +end Smt.Reconstruct.Int.Tactic + +example (x y z : Int) : 1 * (x + y) * z = z * y + x * z := by + poly_norm diff --git a/Smt/Reconstruct/Int/Rewrites.lean b/Smt/Reconstruct/Int/Rewrites.lean index f2ab4b10..bae255aa 100644 --- a/Smt/Reconstruct/Int/Rewrites.lean +++ b/Smt/Reconstruct/Int/Rewrites.lean @@ -96,10 +96,7 @@ theorem plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs := Int.neg_eq_neg_one_mul x ▸ Int.add_assoc ts (-x) ss ▸ Int.add_assoc ts (-x + ss) x ▸ Int.add_comm (-x) ss ▸ (Int.neg_add_cancel_right ss x).symm ▸ rfl --- theorem abs_elim : |x| = if x < 0 then -x else x := --- if h : x < 0 then --- if_pos h ▸ abs_of_neg h --- else --- if_neg h ▸ abs_of_nonneg (le_of_not_lt h) +theorem abs_elim : (if x < 0 then -x else x) = if x < 0 then -x else x := + rfl end Smt.Reconstruct.Int.Rewrite diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean new file mode 100644 index 00000000..327c93f3 --- /dev/null +++ b/Smt/Reconstruct/Rat.lean @@ -0,0 +1,430 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct +import Smt.Reconstruct.Builtin.Lemmas +import Smt.Reconstruct.Rat.Core +import Smt.Reconstruct.Rat.Lemmas +import Smt.Reconstruct.Rat.Polynorm +import Smt.Reconstruct.Rat.Rewrites +import Smt.Reconstruct.Rewrite + +namespace Smt.Reconstruct.Rat + +open Lean hiding Rat +open Qq + +@[smt_sort_reconstruct] def reconstructRatSort : SortReconstructor := fun s => do match s.getKind with + | .REAL_SORT => return q(Rat) + | _ => return none + +@[smt_term_reconstruct] def reconstructRat : TermReconstructor := fun t => do match t.getKind with + | .SKOLEM => match t.getSkolemId with + | .DIV_BY_ZERO => return q(fun (x : Rat) => x / 0) + | _ => return none + | .CONST_RATIONAL => + let c : Lean.Rat := t.getRationalValue + let num : Q(Rat) := mkRatLit c.num.natAbs + if c.den == 1 then + if c.num ≥ 0 then + return q($num) + else + return q(-$num) + else + let den : Q(Rat) := mkRatLit c.den + if c.num ≥ 0 then + return q($num / $den) + else + return q(-$num / $den) + | .NEG => + if t.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + return q(-$x) + | .SUB => + if t.getSort.isInteger then return none + leftAssocOp q(@HSub.hSub Rat Rat Rat _) t + | .ADD => + if t.getSort.isInteger then return none + leftAssocOp q(@HAdd.hAdd Rat Rat Rat _) t + | .MULT => + if t.getSort.isInteger then return none + leftAssocOp q(@HMul.hMul Rat Rat Rat _) t + | .DIVISION => + leftAssocOp q(@HDiv.hDiv Rat Rat Rat _) t + | .DIVISION_TOTAL => + leftAssocOp q(@HDiv.hDiv Rat Rat Rat _) t + | .ABS => + if t.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + return q(if $x < 0 then -$x else $x) + | .LEQ => + if t[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + let y : Q(Rat) ← reconstructTerm t[1]! + return q($x ≤ $y) + | .LT => + if t[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + let y : Q(Rat) ← reconstructTerm t[1]! + return q($x < $y) + | .GEQ => + if t[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + let y : Q(Rat) ← reconstructTerm t[1]! + return q($x ≥ $y) + | .GT => + if t[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + let y : Q(Rat) ← reconstructTerm t[1]! + return q($x > $y) + | .TO_REAL => + let x : Q(Int) ← reconstructTerm t[0]! + return q($x : Rat) + | .TO_INTEGER => + let x : Q(Rat) ← reconstructTerm t[0]! + return q(«$x».floor) + | .IS_INTEGER => + let x : Q(Rat) ← reconstructTerm t[0]! + return q($x = «$x».floor) + | _ => return none +where + mkRatLit (n : Nat) : Q(Rat) := + let lit : Q(Nat) := Lean.mkRawNatLit n + q(OfNat.ofNat $lit) + leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do + let mut curr ← reconstructTerm t[0]! + for i in [1:t.getNumChildren] do + curr := mkApp2 op curr (← reconstructTerm t[i]!) + return curr + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match pf.getRewriteRule with + | .ARITH_DIV_BY_CONST_ELIM => + let t : Q(Rat) ← reconstructTerm pf.getResult[0]![0]! + let c : Q(Rat) ← reconstructTerm pf.getResult[0]![1]! + addThm q($t / $c = $t * (1 / $c)) q(@Rewrite.div_by_const_elim $t $c) + | .ARITH_PLUS_ZERO => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_zero) args) + | .ARITH_MUL_ONE => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mul_one) args) + | .ARITH_MUL_ZERO => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mul_zero) args) + | .ARITH_DIV_TOTAL => + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]! + addThm q($t / $s = $t / $s) q(@Rewrite.div_total $t $s $h) + | .ARITH_NEG_NEG_ONE => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(-1 * (-1 * $t) = $t) q(@Rewrite.neg_neg_one $t) + | .ARITH_ELIM_UMINUS => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(-$t = -1 * $t) q(@Rewrite.elim_uminus $t) + | .ARITH_ELIM_MINUS => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q($t - $s = $t + -1 * $s) q(@Rewrite.elim_minus $t $s) + | .ARITH_ELIM_GT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t > $s) = ¬($t ≤ $s)) q(@Rewrite.elim_gt $t $s) + | .ARITH_ELIM_LT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t < $s) = ¬($t ≥ $s)) q(@Rewrite.elim_lt $t $s) + | .ARITH_ELIM_LEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≤ $s) = ($s ≥ $t)) q(@Rewrite.elim_leq $t $s) + | .ARITH_GEQ_NORM1 => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = ($t - $s ≥ 0)) q(@Rewrite.geq_norm1 $t $s) + | .ARITH_GEQ_NORM2 => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = (-$t ≤ -$s)) q(@Rewrite.geq_norm2 $t $s) + | .ARITH_REFL_LEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≤ $t) = True) q(@Rewrite.refl_leq $t) + | .ARITH_REFL_LT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(($t < $t) = False) q(@Rewrite.refl_lt $t) + | .ARITH_REFL_GEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≥ $t) = True) q(@Rewrite.refl_geq $t) + | .ARITH_REFL_GT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(($t > $t) = False) q(@Rewrite.refl_gt $t) + | .ARITH_PLUS_FLATTEN => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_flatten) args) + | .ARITH_MULT_FLATTEN => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mult_flatten) args) + | .ARITH_MULT_DIST => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mult_dist) args) + | .ARITH_PLUS_CANCEL1 => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.plus_cancel1) args) + | .ARITH_PLUS_CANCEL2 => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_cancel2) args) + | .ARITH_ABS_ELIM => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(ite ($t < 0) (-$t) $t = ite ($t < 0) (-$t) $t) q(@Rewrite.abs_elim $t) + | _ => return none +where + reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do + let mut args' := #[] + for arg in args do + let mut arg' := #[] + for subarg in arg do + arg' := arg'.push (← reconstructTerm subarg) + args' := args'.push arg' + return args' + +def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let f := fun (ks, ls, rs, hs) p => do + let l : Q(Rat) ← reconstructTerm p.getResult[0]! + let r : Q(Rat) ← reconstructTerm p.getResult[1]! + let lsl := q($ls + $l) + let rsr := q($rs + $r) + let k := p.getResult.getKind + if ks == .LT && k == .LT then + let hs : Q($ls < $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₁ $hs $h)) + else if ks == .LT && k == .LEQ then + let hs : Q($ls < $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₂ $hs $h)) + else if ks == .LT && k == .EQUAL then + let hs : Q($ls < $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₃ $hs $h)) + else if ks == .LEQ && k == .LT then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₄ $hs $h)) + else if ks == .LEQ && k == .LEQ then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Rat.sum_ub₅ $hs $h)) + else if ks == .LEQ && k == .EQUAL then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Rat.sum_ub₆ $hs $h)) + else if ks == .EQUAL && k == .LT then + let hs : Q($ls = $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₇ $hs $h)) + else if ks == .EQUAL && k == .LEQ then + let hs : Q($ls = $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Rat.sum_ub₈ $hs $h)) + else if ks == .EQUAL && k == .EQUAL then + let hs : Q($ls = $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.EQUAL, lsl, rsr, q(Rat.sum_ub₉ $hs $h)) + else + throwError "[sum_ub]: invalid kinds: {ks}, {p.getResult.getKind}" + let k := pf.getChildren[0]!.getResult.getKind + let ls : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let rs : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let hs ← reconstructProof pf.getChildren[0]! + let (_, ls, rs, hs) ← pf.getChildren[1:].foldlM f (k, ls, rs, hs) + addThm q($ls < $rs) hs + +def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let ts := pf.getResult[0]!.getChildren + let mut hs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + let mut map : HashMap cvc5.Term Nat := {} + for h : i in [0:ts.size] do + let t := ts[i]'(h.right) + let p : Q(Prop) ← reconstructTerm t + hs := hs.push (Name.num `a i, fun _ => return p) + map := map.insert (if t.getKind == .NOT then t[0]![0]! else t[0]!) i + let t := pf.getResult[1]! + let vs := if t[0]!.getKind == .CONST_INTEGER then t[1]!.getChildren else t[0]!.getChildren + let f t ps := do + let p : Q(Prop) ← reconstructTerm t + return q($p :: $ps) + let ps : Q(List Prop) ← ts.foldrM f q([]) + let q : Q(Prop) ← reconstructTerm t + let h : Q(impliesN $ps $q) ← Meta.withLocalDeclsD hs fun hs => do + let h : Q($q) ← if ts[map.find! vs[0]!]!.getKind == .NOT then + let a : Q(Rat) ← reconstructTerm vs[0]! + let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]! + go vs ts hs map .GT q($a * $a) q(Rat.mul_sign₀ $ha) 2 + else + let a : Q(Rat) ← reconstructTerm vs[0]! + go vs ts hs map ts[map.find! vs[0]!]!.getKind a hs[map.find! vs[0]!]! 1 + Meta.mkLambdaFVars hs h + addThm q(andN $ps → $q) q(Builtin.scopes $h) +where + go vs ts hs map ka (a : Q(Rat)) (ha : Expr) i : ReconstructM Expr := do + if hi : i < vs.size then + let b : Q(Rat) ← reconstructTerm vs[i] + let k := ts[map.find! vs[i]]!.getKind + if ka == .LT && k == .LT then + let ha : Q($a < 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Rat.mul_sign₁ $ha $hb) (i + 1) + else if ka == .LT && k == .NOT then + let ha : Q($a < 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b * $b) q(Rat.mul_sign₂ $ha $hb) (i + 2) + else if ka == .LT && k == .GT then + let ha : Q($a < 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Rat.mul_sign₃ $ha $hb) (i + 1) + else if ka == .GT && k == .LT then + let ha : Q($a > 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Rat.mul_sign₄ $ha $hb) (i + 1) + else if ka == .GT && k == .NOT then + let ha : Q($a > 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b * $b) q(Rat.mul_sign₅ $ha $hb) (i + 2) + else if ka == .GT && k == .GT then + let ha : Q($a > 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Rat.mul_sign₆ $ha $hb) (i + 1) + else + throwError "[mul_sign]: invalid kinds: {ka}, {k}" + else + return ha + +@[smt_proof_reconstruct] def reconstructRatProof : ProofReconstructor := fun pf => do match pf.getRule with + | .DSL_REWRITE + | .THEORY_REWRITE => reconstructRewrite pf + | .ARITH_SUM_UB => + if pf.getResult[0]!.getSort.isInteger then return none + reconstructSumUB pf + | .INT_TIGHT_UB => + let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let c : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let h : Q($i < $c) ← reconstructProof pf.getChildren[0]! + addThm q($i ≤ «$c».floor) q(@Rat.int_tight_ub $c $i $h) + | .INT_TIGHT_LB => + let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let c : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let h : Q($i > $c) ← reconstructProof pf.getChildren[0]! + addThm q($i ≥ «$c».ceil) q(@Rat.int_tight_lb $c $i $h) + | .ARITH_TRICHOTOMY => + if pf.getResult[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm pf.getResult[0]! + let c : Q(Rat) ← reconstructTerm pf.getResult[1]! + let k₁ := pf.getChildren[0]!.getResult.getKind + let k₂ := pf.getChildren[1]!.getResult.getKind + if k₁ == .GEQ && k₂ == .NOT then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Rat.trichotomy₁ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .GEQ then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Rat.trichotomy₂ $h₁ $h₂) + else if k₁ == .GEQ && k₂ == .LEQ then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Rat.trichotomy₃ $h₁ $h₂) + else if k₁ == .LEQ && k₂ == .GEQ then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Rat.trichotomy₄ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .LT then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Rat.trichotomy₅ $h₁ $h₂) + else if k₁ == .LT && k₂ == .NOT then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Rat.trichotomy₆ $h₁ $h₂) + else + return none + | .ARITH_POLY_NORM => + if pf.getResult[0]!.getSort.isInteger then return none + let a : Q(Rat) ← reconstructTerm pf.getResult[0]! + let b : Q(Rat) ← reconstructTerm pf.getResult[1]! + addTac q($a = $b) Rat.polyNorm + | .ARITH_MULT_SIGN => + if pf.getResult[1]![0]!.getSort.isInteger then return none + reconstructMulSign pf + | .ARITH_MULT_POS => + if pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Rat) ← reconstructTerm pf.getArguments[0]! + let l : Q(Rat) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Rat) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m > 0 ∧ $l < $r → $m * $l < $m * $r) q(@Rat.mul_pos_lt $l $r $m) + | .LEQ => + addThm q($m > 0 ∧ $l ≤ $r → $m * $l ≤ $m * $r) q(@Rat.mul_pos_le $l $r $m) + | .EQUAL => + addThm q($m > 0 ∧ $l = $r → $m * $l = $m * $r) q(@Rat.mul_pos_eq $l $r $m) + | .GEQ => + addThm q($m > 0 ∧ $l ≥ $r → $m * $l ≥ $m * $r) q(@Rat.mul_pos_ge $l $r $m) + | .GT => + addThm q($m > 0 ∧ $l > $r → $m * $l > $m * $r) q(@Rat.mul_pos_gt $l $r $m) + | _ => return none + | .ARITH_MULT_NEG => + if pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Rat) ← reconstructTerm pf.getArguments[0]! + let l : Q(Rat) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Rat) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m < 0 ∧ $l < $r → $m * $l > $m * $r) q(@Rat.mul_neg_lt $l $r $m) + | .LEQ => + addThm q($m < 0 ∧ $l ≤ $r → $m * $l ≥ $m * $r) q(@Rat.mul_neg_le $l $r $m) + | .EQUAL => + addThm q($m < 0 ∧ $l = $r → $m * $l = $m * $r) q(@Rat.mul_neg_eq $l $r $m) + | .GEQ => + addThm q($m < 0 ∧ $l ≥ $r → $m * $l ≤ $m * $r) q(@Rat.mul_neg_ge $l $r $m) + | .GT => + addThm q($m < 0 ∧ $l > $r → $m * $l < $m * $r) q(@Rat.mul_neg_gt $l $r $m) + | _ => return none + | .ARITH_MULT_TANGENT => + let x : Q(Rat) ← reconstructTerm pf.getArguments[0]! + let y : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let a : Q(Rat) ← reconstructTerm pf.getArguments[2]! + let b : Q(Rat) ← reconstructTerm pf.getArguments[3]! + if pf.getArguments[4]!.getIntegerValue == -1 then + addThm q(($x * $y ≤ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≥ $b ∨ $x ≥ $a ∧ $y ≤ $b)) q(@Rat.mul_tangent_lower_eq $a $b $x $y) + else + addThm q(($x * $y ≥ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≤ $b ∨ $x ≥ $a ∧ $y ≥ $b)) q(@Rat.mul_tangent_upper_eq $a $b $x $y) + | _ => return none + +end Smt.Reconstruct.Rat + diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean new file mode 100644 index 00000000..91f2e218 --- /dev/null +++ b/Smt/Reconstruct/Rat/Core.lean @@ -0,0 +1,177 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Batteries.Data.Rat + + +namespace Int +@[simp] +protected theorem natCast_eq_zero {n : Nat} : (n : Int) = 0 ↔ n = 0 := by + omega + +protected theorem natCast_ne_zero {n : Nat} : (n : Int) ≠ 0 ↔ n ≠ 0 := by + exact not_congr Int.natCast_eq_zero + +protected theorem gcd_def (i j : Int) : i.gcd j = i.natAbs.gcd j.natAbs := + rfl + +protected theorem gcd_def' (i : Int) (j : Nat) : i.gcd (ofNat j) = i.natAbs.gcd j := + Int.gcd_def _ _ + +theorem gcd_eq_zero_iff {i j : Int} : gcd i j = 0 ↔ i = 0 ∧ j = 0 := by + rw [gcd, Nat.gcd_eq_zero_iff, natAbs_eq_zero, natAbs_eq_zero] + +theorem gcd_ne_zero_iff {i j : Int} : gcd i j ≠ 0 ↔ i ≠ 0 ∨ j ≠ 0 := by + constructor + · intro h + let tmp := not_congr gcd_eq_zero_iff |>.mp h + if h_i : i = 0 then + simp [h_i] at tmp + exact Or.inr tmp + else + exact Or.inl h_i + · intro h gcd_zero + rw [gcd_eq_zero_iff] at gcd_zero + simp [gcd_zero.1, gcd_zero.2] at h + +protected theorem dvd_mul_left_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ k * j +| ⟨n, h⟩ => by + rw [h] + exists k * n + rw [ + ← Int.mul_assoc k i n, + Int.mul_comm k i, + Int.mul_assoc i k n, + ] + +protected theorem dvd_mul_right_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ j * k := + Int.mul_comm j k ▸ Int.dvd_mul_left_of_dvd k + +theorem flatten_div_mul_eq_mul_div + {i1 i2 i3 i4 j : Int} + (j_pos : j ≠ 0) + (j_dvd_i1 : j ∣ i1) + (j_dvd_i4 : j ∣ i4) +: i1 / j * i2 = i3 * (i4 / j) → i1 * i2 = i3 * i4 := by + intro h + rw [← Int.mul_eq_mul_left_iff j_pos] at h + conv at h => + lhs + rw [← Int.mul_assoc] + rw [← Int.mul_ediv_assoc _ j_dvd_i1] + rw [Int.mul_ediv_cancel_left _ j_pos] + conv at h => + rhs + rw [← Int.mul_assoc] + conv => lhs ; rw [Int.mul_comm] + rw [Int.mul_assoc] + rw [← Int.mul_ediv_assoc _ j_dvd_i4] + rw [Int.mul_ediv_cancel_left _ j_pos] + assumption +end Int + + + +namespace Rat + +theorem num_divInt_den (q : Rat) : q.num /. q.den = q := + divInt_self _ + +theorem mk'_eq_divInt {n d h c} : (⟨n, d, h, c⟩ : Rat) = n /. d := + (num_divInt_den _).symm + +@[elab_as_elim] +def numDenCasesOn.{u} {C : Rat → Sort u} +: ∀ (a : Rat) (_ : ∀ n d, 0 < d → (Int.natAbs n).Coprime d → C (n /. d)), C a +| ⟨n, d, h, c⟩, H => by rw [mk'_eq_divInt]; exact H n d (Nat.pos_of_ne_zero h) c + +@[elab_as_elim] +def numDenCasesOn'.{u} {C : Rat → Sort u} (a : Rat) + (H : ∀ (n : Int) (d : Nat), d ≠ 0 → C (n /. d)) +: C a := + numDenCasesOn a fun n d h _ => H n d (Nat.pos_iff_ne_zero.mp h) + +@[elab_as_elim] +def numDenCasesOn''.{u} {C : Rat → Sort u} (a : Rat) + (H : ∀ (n : Int) (d : Nat) (nz red), C (mk' n d nz red)) +: C a := + numDenCasesOn a fun n d h h' ↦ by + let h_pos := Nat.pos_iff_ne_zero.mp h + rw [← mk_eq_divInt _ _ h_pos h'] + exact H n d h_pos _ + + + +protected theorem add_comm (a b : Rat) : a + b = b + a := by + simp [add_def, Int.add_comm, Int.mul_comm, Nat.mul_comm] + +protected theorem add_zero : ∀ a : Rat, a + 0 = a +| ⟨num, den, _h, _h'⟩ => by + simp [Rat.add_def] + simp only [Rat.normalize_eq_mkRat, Rat.mk_eq_normalize] + +protected theorem zero_add : ∀ a : Rat, 0 + a = a := + fun a => Rat.add_comm a 0 ▸ Rat.add_zero a + +protected theorem eq_mkRat : ∀ a : Rat, a = mkRat a.num a.den := fun a => by + simp [Rat.mkRat_def, a.den_nz, Rat.normalize_eq, a.reduced] + +protected theorem mul_eq_zero_iff : ∀ {a b : Rat}, a * b = 0 ↔ a = 0 ∨ b = 0 := by + intro a b + constructor + · simp only [Rat.mul_def, Rat.normalize_eq_zero] + intro h + cases Int.mul_eq_zero.mp h + · apply Or.inl + rw [Rat.eq_mkRat a, Rat.mkRat_eq_zero] + assumption + exact a.den_nz + · apply Or.inr + rw [Rat.eq_mkRat b, Rat.mkRat_eq_zero] + assumption + exact b.den_nz + · intro + | .inl h => simp only [h, Rat.zero_mul] + | .inr h => simp only [h, Rat.mul_zero] + +protected theorem mul_ne_zero_iff : ∀ {a b : Rat}, a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by + intro a b + simp only [not_congr (@Rat.mul_eq_zero_iff a b), not_or, ne_eq] + +protected theorem normalize_den_ne_zero +: ∀ {d : Int} {n : Nat}, (h : n ≠ 0) → (normalize d n h).den ≠ 0 := by + intro d n nz + simp only [Rat.normalize_eq, ne_eq] + intro h + apply nz + rw [← Nat.zero_mul (d.natAbs.gcd n)] + apply Nat.div_eq_iff_eq_mul_left _ _ |>.mp + · assumption + · exact Nat.gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero nz) + · exact Nat.gcd_dvd_right _ _ + + + +protected theorem add_assoc (a b c : Rat) : a + b + c = a + (b + c) := + numDenCasesOn' a fun n₁ d₁ h₁ ↦ + numDenCasesOn' b fun n₂ d₂ h₂ ↦ + numDenCasesOn' c fun n₃ d₃ h₃ ↦ by + simp only [ + ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, + divInt_add_divInt, Int.mul_eq_zero, or_self, h₃ + ] + rw [Int.mul_assoc, Int.add_mul, Int.add_mul, Int.mul_assoc, Int.add_assoc] + congr 2 + ac_rfl + +protected theorem mul_assoc (a b c : Rat) : a + b + c = a + (b + c) := + numDenCasesOn' a fun n₁ d₁ _h₁ => + numDenCasesOn' b fun n₂ d₂ _h₂ => + numDenCasesOn' c fun n₃ d₃ _h₃ => by + simp only [Rat.divInt_ofNat] + exact Rat.add_assoc _ _ _ +end Rat diff --git a/Smt/Reconstruct/Rat/Lemmas.lean b/Smt/Reconstruct/Rat/Lemmas.lean new file mode 100644 index 00000000..277da250 --- /dev/null +++ b/Smt/Reconstruct/Rat/Lemmas.lean @@ -0,0 +1,210 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed +-/ + +import Batteries.Data.Rat + +private theorem Rat.mul_lt_mul_left {c x y : Rat} (hc : c > 0) : (c * x < c * y) = (x < y) := by + sorry + +private theorem Rat.mul_le_mul_left {c x y : Rat} (hc : c > 0) : (c * x ≤ c * y) = (x ≤ y) := by + sorry + +private theorem Rat.mul_eq_zero_left {x y : Rat} (hx : x ≠ 0) (hxy : x * y = 0) : y = 0 := by + sorry + +private def uncurry {p₁ p₂ p₃ : Prop} : (p₁ → p₂ → p₃) → (p₁ ∧ p₂) → p₃ := by + intros h₁ h₂ + have ⟨ht₁, ht₂⟩ := h₂ + exact h₁ ht₁ ht₂ + +namespace Smt.Reconstruct.Rat + +variable {a b c d : Rat} + +theorem sum_ub₁ (h₁ : a < b) (h₂ : c < d) : a + c < b + d := by + sorry + +theorem sum_ub₂ (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := by + sorry + +theorem sum_ub₃ (h₁ : a < b) (h₂ : c = d) : a + c < b + d := by + sorry + +theorem sum_ub₄ (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d := by + sorry + +theorem sum_ub₅ (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := by + sorry + +theorem sum_ub₆ (h₁ : a ≤ b) (h₂ : c = d) : a + c ≤ b + d := by + sorry + +theorem sum_ub₇ (h₁ : a = b) (h₂ : c < d) : a + c < b + d := by + sorry + +theorem sum_ub₈ (h₁ : a = b) (h₂ : c ≤ d) : a + c ≤ b + d := by + sorry + +theorem sum_ub₉ (h₁ : a = b) (h₂ : c = d) : a + c ≤ b + d := by + sorry + +theorem neg_lt_neg (h : a < b) : -a > -b := by + sorry + +theorem neg_le_neg (h : a ≤ b) : -a ≥ -b := by + sorry + +theorem int_tight_ub {i : Int} (h : i < c) : i ≤ c.floor := by + sorry + +theorem int_tight_lb {i : Int} (h : i > c) : i ≥ c.ceil := by + sorry + +theorem trichotomy₁ (h₁ : a ≥ b) (h₂ : a ≠ b) : a > b := by + sorry + +theorem trichotomy₂ (h₁ : a ≠ b) (h₂ : a ≥ b) : a > b := by + sorry + +theorem trichotomy₃ (h₁ : a ≥ b) (h₂ : a ≤ b) : a = b := by + sorry + +theorem trichotomy₄ (h₁ : a ≤ b) (h₂ : a ≥ b) : a = b := by + sorry + +theorem trichotomy₅ (h₁ : a ≠ b) (h₂ : a ≤ b) : a < b := by + sorry + +theorem trichotomy₆ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by + sorry + +theorem lt_eq_sub_lt_zero : (a < b) = (a - b < 0) := by + sorry + +theorem le_eq_sub_le_zero : (a ≤ b) = (a - b ≤ 0) := by + sorry + +theorem eq_eq_sub_eq_zero : (a = b) = (a - b = 0) := by + sorry + +theorem ge_eq_sub_ge_zero : (a ≥ b) = (a - b ≥ 0) := by + sorry + +theorem gt_eq_sub_gt_zero : (a > b) = (a - b > 0) := by + sorry + +theorem lt_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) < 0) = (x - y < 0) := by + rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, Rat.mul_lt_mul_left hc] + rw [lt_eq_sub_lt_zero, @lt_eq_sub_lt_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem le_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≤ a₂) = (b₁ ≤ b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) ≤ 0) = (x - y ≤ 0) := by + rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, Rat.mul_le_mul_left hc] + rw [le_eq_sub_le_zero, @le_eq_sub_le_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem eq_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ = a₂) = (b₁ = b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) = 0) = (x - y = 0) := by + apply propext; constructor + · apply Rat.mul_eq_zero_left sorry + · intro hxy; rw [hxy, Rat.mul_zero] + rw [@eq_eq_sub_eq_zero a₁, @eq_eq_sub_eq_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem ge_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≥ a₂) = (b₁ ≥ b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) ≥ 0) = (x - y ≥ 0) := by + rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, ge_iff_le, Rat.mul_le_mul_left hc] + rw [ge_eq_sub_ge_zero, @ge_eq_sub_ge_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem gt_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ > a₂) = (b₁ > b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) > 0) = (x - y > 0) := by + rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, gt_iff_lt, Rat.mul_lt_mul_left hc] + rw [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem mul_sign₁ (ha : a < 0) (hb : b < 0) : a * b > 0 := by + sorry + +theorem mul_sign₃ (ha : a < 0) (hb : b > 0) : a * b < 0 := by + sorry + +theorem mul_sign₄ (ha : a > 0) (hb : b < 0) : a * b < 0 := by + sorry + +theorem mul_sign₆ (ha : a > 0) (hb : b > 0) : a * b > 0 := by + sorry + +theorem mul_sign₀ (ha : a ≠ 0) : a * a > 0 := + sorry + +theorem mul_sign₂ (ha : a < 0) (hb : b ≠ 0) : a * b * b < 0 := + sorry + +theorem mul_sign₅ (ha : a > 0) (hb : b ≠ 0) : a * b * b > 0 := + sorry + +theorem mul_pos_lt (h : c > 0 ∧ a < b) : c * a < c * b := + sorry + +theorem mul_pos_le (h : c > 0 ∧ a ≤ b) : c * a ≤ c * b := + sorry + +theorem mul_pos_gt (h : c > 0 ∧ a > b) : c * a > c * b := + mul_pos_lt h + +theorem mul_pos_ge (h : c > 0 ∧ a ≥ b) : c * a ≥ c * b := + mul_pos_le h + +theorem mul_pos_eq (h : c > 0 ∧ a = b) : c * a = c * b := by + rw [h.2] + +theorem mul_neg_lt (h : c < 0 ∧ a < b) : c * a > c * b := + sorry + +theorem mul_neg_le (h : c < 0 ∧ a ≤ b) : c * a ≥ c * b := + sorry + +theorem mul_neg_gt (h : c < 0 ∧ a > b) : c * a < c * b := + mul_neg_lt h + +theorem mul_neg_ge (h : c < 0 ∧ a ≥ b) : c * a ≤ c * b := + mul_neg_le h + +theorem mul_neg_eq (h : c < 0 ∧ a = b) : c * a = c * b := by + rw [h.2] + +theorem mul_tangent_mp_lower (h : x * y ≤ b * x + a * y - a * b) + : x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b := + sorry + +theorem mul_tangent_mpr_lower (h : x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b) + : x * y ≤ b * x + a * y - a * b := + sorry + +theorem mul_tangent_lower : + x * y ≤ b * x + a * y - a * b ↔ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b := + ⟨mul_tangent_mp_lower, mul_tangent_mpr_lower⟩ + +theorem mul_tangent_lower_eq + : (x * y ≤ b * x + a * y - a * b) = (x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b) := + propext (mul_tangent_lower) + +theorem mul_tangent_mp_upper (h : x * y ≥ b * x + a * y - a * b) + : x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b := + sorry + +theorem mul_tangent_mpr_upper (h : x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b) + : x * y ≥ b * x + a * y - a * b := + sorry + +theorem mul_tangent_upper + : x * y ≥ b * x + a * y - a * b ↔ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b := + ⟨mul_tangent_mp_upper, mul_tangent_mpr_upper⟩ + +theorem mul_tangent_upper_eq + : (x * y ≥ b * x + a * y - a * b) = (x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b) := + propext (mul_tangent_upper) + +end Smt.Reconstruct.Rat diff --git a/Smt/Reconstruct/Rat/Polynorm.lean b/Smt/Reconstruct/Rat/Polynorm.lean new file mode 100644 index 00000000..ee770609 --- /dev/null +++ b/Smt/Reconstruct/Rat/Polynorm.lean @@ -0,0 +1,279 @@ +/- +Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Batteries.Data.Rat + +import Lean +import Qq + +theorem Rat.neg_mul_eq_neg_mul (a b : Rat) : -(a * b) = -a * b := by + sorry + +@[simp] theorem Rat.zero_add (a : Rat) : 0 + a = a := by + simp [add_def, normalize_eq_mkRat, Int.add_comm, Nat.add_comm, mkRat_self] + +namespace Smt.Reconstruct.Rat.PolyNorm + +abbrev Var := Nat + +def Context := Var → Rat + +structure Monomial where + coeff : Rat + vars : List Var +deriving Inhabited, Repr + +namespace Monomial + +open Qq in +def toExpr (m : Monomial) (ppCtx : Var → Q(Rat)) : Q(Rat) := + if h : m.vars = [] then + toExprCoeff m.coeff + else + if m.coeff = 1 then + (m.vars.drop 1).foldl (fun acc v => q($acc * $(ppCtx v))) (ppCtx (m.vars.head h)) + else + m.vars.foldl (fun acc v => q($acc * $(ppCtx v))) (toExprCoeff m.coeff) +where + toExprCoeff (c : Rat) : Q(Rat) := + let num : Q(Rat) := mkRatLit c.num.natAbs + if c.den == 1 then + if c.num ≥ 0 then + q($num) + else + q(-$num) + else + let den : Q(Rat) := mkRatLit c.den + if c.num ≥ 0 then + q($num / $den) + else + q(-$num / $den) + mkRatLit (n : Nat) : Q(Rat) := + let l : Q(Nat) := Lean.mkRawNatLit n + q(OfNat.ofNat $l) + +def neg (m : Monomial) : Monomial := + { m with coeff := -m.coeff } + +def add (m₁ m₂ : Monomial) (_ : m₁.vars = m₂.vars) : Monomial := + { coeff := m₁.coeff + m₂.coeff, vars := m₁.vars } + +-- Invariant: monomial variables remain sorted. +def mul (m₁ m₂ : Monomial) : Monomial := + let coeff := m₁.coeff * m₂.coeff + let vars := m₁.vars.foldr insert m₂.vars + { coeff, vars } +where + insert (x : Var) : List Var → List Var + | [] => [x] + | y :: ys => if x ≤ y then x :: y :: ys else y :: insert x ys + +def divConst (m : Monomial) (c : Rat) : Monomial := + { m with coeff := m.coeff / c } + +def denote (ctx : Context) (m : Monomial) : Rat := + m.coeff * m.vars.foldl (fun acc v => acc * ctx v) 1 + +theorem denote_neg {m : Monomial} : m.neg.denote ctx = -m.denote ctx := by + simp only [neg, denote, Rat.neg_mul_eq_neg_mul] + +theorem denote_mul {m₁ m₂ : Monomial} : (m₁.mul m₂).denote ctx = m₁.denote ctx * m₂.denote ctx := + sorry + +theorem denote_divConst {m : Monomial} : (m.divConst c).denote ctx = m.denote ctx / c := + sorry + +end Monomial + +abbrev Polynomial := List Monomial + +namespace Polynomial + +open Qq in +def toExpr (p : Polynomial) (ppCtx : Var → Q(Rat)) : Q(Rat) := + go p +where + go : Polynomial → Q(Rat) + | [] => q(0) + | [m] => m.toExpr ppCtx + | m :: ms =>q($(m.toExpr ppCtx) + $(go ms)) + +def neg (p : Polynomial) : Polynomial := + p.map Monomial.neg + +-- NOTE: implementation merges monomials with same variables. +-- Invariant: monomials remain sorted. +def add (p q : Polynomial) : Polynomial := + p.foldr insert q +where + insert (m : Monomial) : Polynomial → Polynomial + | [] => [m] + | n :: ns => + if m.vars < n.vars then + m :: n :: ns + else if h : m.vars = n.vars then + let m' := m.add n h + if m'.coeff = 0 then ns else m' :: ns + else + n :: insert m ns + +def sub (p q : Polynomial) : Polynomial := + p.add q.neg + +-- Invariant: monomials remain sorted. +def mulMonomial (m : Monomial) (p : Polynomial) : Polynomial := + p.foldr (fun n acc => Polynomial.add [m.mul n] acc) [] + +-- Invariant: monomials remain sorted. +def mul (p q : Polynomial) : Polynomial := + p.foldl (fun acc m => (q.mulMonomial m).add acc) [] + +def divConst (p : Polynomial) (c : Rat) : Polynomial := + p.map (·.divConst c) + +def denote (ctx : Context) (p : Polynomial) : Rat := + p.foldl (fun acc m => acc + m.denote ctx) 0 + +theorem denote_neg {p : Polynomial} : p.neg.denote ctx = -p.denote ctx := + sorry + +theorem denote_add {p q : Polynomial} : (p.add q).denote ctx = p.denote ctx + q.denote ctx := + sorry + +theorem denote_sub {p q : Polynomial} : (p.sub q).denote ctx = p.denote ctx - q.denote ctx := by + simp only [sub, denote_neg, denote_add, Rat.sub_eq_add_neg] + +theorem denote_mulMonomial {p : Polynomial} : (p.mulMonomial m).denote ctx = m.denote ctx * p.denote ctx := + sorry + +theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.denote ctx := + sorry + +theorem denote_divConst {p : Polynomial} : (p.divConst c).denote ctx = p.denote ctx / c := by + sorry + +end Polynomial + +inductive Expr where + | val (v : Rat) + | var (v : Nat) + | neg (a : Expr) + | add (a b : Expr) + | sub (a b : Expr) + | mul (a b : Expr) + | divConst (a : Expr) (c : Rat) +deriving Inhabited, Repr + +namespace Expr + +def toPolynomial : Expr → Polynomial + | val v => if v = 0 then [] else [{ coeff := v, vars := [] }] + | var v => [{ coeff := 1, vars := [v] }] + | neg a => a.toPolynomial.neg + | add a b => Polynomial.add a.toPolynomial b.toPolynomial + | sub a b => Polynomial.sub a.toPolynomial b.toPolynomial + | mul a b => Polynomial.mul a.toPolynomial b.toPolynomial + | divConst a c => Polynomial.divConst a.toPolynomial c + +def denote (ctx : Context) : Expr → Rat + | val v => v + | var v => ctx v + | neg a => -a.denote ctx + | add a b => a.denote ctx + b.denote ctx + | sub a b => a.denote ctx - b.denote ctx + | mul a b => a.denote ctx * b.denote ctx + | divConst a c => a.denote ctx / c + +theorem denote_toPolynomial {e : Expr} : e.denote ctx = e.toPolynomial.denote ctx := by + induction e with + | val v => + simp only [denote, toPolynomial] + split <;> rename_i hv + · rewrite [hv]; rfl + · simp [Polynomial.denote, Monomial.denote] + | var v => + simp [denote, toPolynomial, Polynomial.denote, Monomial.denote] + | neg a ih => + simp only [denote, toPolynomial, Polynomial.denote_neg, ih] + | add a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_add, ih₁, ih₂] + | sub a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_sub, ih₁, ih₂] + | mul a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_mul, ih₁, ih₂] + | divConst a c ih => + simp only [denote, toPolynomial, Polynomial.denote_divConst, ih] + +theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : Expr} (h : e₁.toPolynomial = e₂.toPolynomial) : e₁.denote ctx = e₂.denote ctx := by + rw [denote_toPolynomial, denote_toPolynomial, h] + +end PolyNorm.Expr + +open Lean hiding Rat +open Qq + +abbrev PolyM := StateT (Array Q(Rat)) MetaM + +def getIndex (e : Q(Rat)) : PolyM Nat := do + let es ← get + if let some i := es.findIdx? (· == e) then + return i + else + let size := es.size + set (es.push e) + return size + +partial def toRatConst (e : Q(Rat)) : PolyM Rat := do + match e with + | ~q(OfNat.ofNat $n) => pure n.rawNatLit?.get! + | ~q(-$x) => pure (-(← toRatConst x)) + | ~q($x + $y) => pure ((← toRatConst x) + (← toRatConst y)) + | ~q($x - $y) => pure ((← toRatConst x) - (← toRatConst y)) + | ~q($x * $y) => pure ((← toRatConst x) * (← toRatConst y)) + | ~q($x / $y) => pure ((← toRatConst x) / (← toRatConst y)) + | e => throwError "[poly_norm] a rational number, got {e}" + +partial def toArithExpr (e : Q(Rat)) : PolyM Q(PolyNorm.Expr) := do + match e with + | ~q(OfNat.ofNat $n) => pure q(.val (@OfNat.ofNat Rat $n _)) + | ~q(-$x) => pure q(.neg $(← toArithExpr x)) + | ~q($x + $y) => pure q(.add $(← toArithExpr x) $(← toArithExpr y)) + | ~q($x - $y) => pure q(.sub $(← toArithExpr x) $(← toArithExpr y)) + | ~q($x * $y) => pure q(.mul $(← toArithExpr x) $(← toArithExpr y)) + | ~q($x / $y) => pure q(.divConst $(← toArithExpr x) $(PolyNorm.Monomial.toExpr.toExprCoeff (← toRatConst y))) + | e => let v : Nat ← getIndex e; pure q(.var $v) + +def polyNorm (mv : MVarId) : MetaM Unit := do + let some (_, l, r) := (← mv.getType).eq? + | throwError "[poly_norm] expected an equality, got {← mv.getType}" + let (l, es) ← (toArithExpr l).run #[] + let (r, es) ← (toArithExpr r).run es + let is : Q(Array Rat) := es.foldl (fun acc e => q(«$acc».push $e)) q(#[]) + let ctx : Q(PolyNorm.Context) := q(fun v => if h : v < «$is».size then $is[v] else 0) + let h : Q(«$l».toPolynomial = «$r».toPolynomial) := .app q(@Eq.refl.{1} PolyNorm.Polynomial) q(«$l».toPolynomial) + mv.assign q(@PolyNorm.Expr.denote_eq_from_toPolynomial_eq $ctx $l $r $h) +where + logPolynomial (e : Q(PolyNorm.Expr)) (es : Array Q(Rat)) := do + let p ← unsafe Meta.evalExpr PolyNorm.Expr q(PolyNorm.Expr) e + let ppCtx := fun v => if h : v < es.size then es[v] else q(0) + logInfo m!"poly := {PolyNorm.Polynomial.toExpr p.toPolynomial ppCtx}" + +namespace Tactic + +syntax (name := polyNorm) "poly_norm" : tactic + +open Lean.Elab Tactic in +@[tactic polyNorm] def evalPolyNorm : Tactic := fun _ => + withMainContext do + let mv ← Tactic.getMainGoal + Rat.polyNorm mv + replaceMainGoal [] + +end Smt.Reconstruct.Rat.Tactic + +example (x y z : Rat) : 1 * (x + y) * z / 4 = 1/(2 * 2) * (z * y + x * z) := by + poly_norm diff --git a/Smt/Reconstruct/Rat/Rewrites.lean b/Smt/Reconstruct/Rat/Rewrites.lean new file mode 100644 index 00000000..20eda57d --- /dev/null +++ b/Smt/Reconstruct/Rat/Rewrites.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Batteries.Data.Rat + +namespace Smt.Reconstruct.Rat.Rewrite + +open Function + +theorem div_by_const_elim {t c : Rat} : t / c = t * (1 / c) := + sorry + +-- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites + +variable {t ts x xs : Rat} + +theorem plus_zero : ts + 0 + ss = ts + ss := + sorry + +theorem mul_one : ts * 1 * ss = ts * ss := + (_root_.Rat.mul_one ts).symm ▸ rfl +theorem mul_zero : ts * 0 * ss = 0 := + (_root_.Rat.mul_zero ts).symm ▸ (Rat.zero_mul ss).symm ▸ rfl + +theorem div_total : s ≠ 0 → t / s = t / s := + const _ rfl + +theorem neg_neg_one : -1 * (-1 * t) = t := + sorry + +-- Eliminations + +theorem elim_uminus : -t = -1 * t := + sorry +theorem elim_minus : t - s = t + -1 * s := + sorry +theorem elim_gt : (t > s) = ¬(t ≤ s) := + sorry +theorem elim_lt : (t < s) = ¬(t ≥ s) := + sorry +theorem elim_leq : (t ≤ s) = (s ≥ t) := + propext ge_iff_le + +theorem geq_norm1 : (t ≥ s) = (t - s ≥ 0) := + sorry + +theorem geq_norm2 : (t ≥ s) = (-t ≤ -s) := + sorry + +theorem refl_leq : (t ≤ t) = True := + sorry +theorem refl_lt : (t < t) = False := + sorry +theorem refl_geq : (t ≥ t) = True := + sorry +theorem refl_gt : (t > t) = False := + sorry + +theorem eq_elim : (t = s) = (t ≥ s ∧ t ≤ s) := + sorry + +theorem plus_flatten : xs + (w + ys) + zs = xs + w + ys + zs := + sorry + +theorem mult_flatten : xs * (w * ys) * zs = xs * w * ys * zs := + sorry + +theorem mult_dist : x * (y + z + ws) = x * y + x * (z + ws) := + sorry + +theorem plus_cancel1 : ts + x + ss + (-1 * x) + rs = ts + ss + rs := + sorry +theorem plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs := + sorry + +theorem abs_elim : (if x < 0 then -x else x) = if x < 0 then -x else x := + rfl + +end Smt.Reconstruct.Rat.Rewrite From 02ad87746b445ef168d0b2af0d32d5ebf5e0ee06 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Wed, 19 Jun 2024 19:23:19 +0200 Subject: [PATCH 2/6] chore: Int/Rat lemmas --- Smt/Reconstruct/Int.lean | 1 + Smt/Reconstruct/Int/Core.lean | 130 ++++++++++++++++++++++++++++++ Smt/Reconstruct/Rat/Core.lean | 146 +++++++++++++++++++--------------- 3 files changed, 211 insertions(+), 66 deletions(-) create mode 100644 Smt/Reconstruct/Int/Core.lean diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean index 89e8d742..83a7a79d 100644 --- a/Smt/Reconstruct/Int.lean +++ b/Smt/Reconstruct/Int.lean @@ -7,6 +7,7 @@ Authors: Abdalrhman Mohamed import Smt.Reconstruct import Smt.Reconstruct.Builtin.Lemmas +import Smt.Reconstruct.Int.Core import Smt.Reconstruct.Int.Lemmas import Smt.Reconstruct.Int.Polynorm import Smt.Reconstruct.Int.Rewrites diff --git a/Smt/Reconstruct/Int/Core.lean b/Smt/Reconstruct/Int/Core.lean new file mode 100644 index 00000000..7b569139 --- /dev/null +++ b/Smt/Reconstruct/Int/Core.lean @@ -0,0 +1,130 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed +-/ + +import Batteries.Data.Int + + + +namespace Int +@[simp] +protected theorem natCast_eq_zero {n : Nat} : (n : Int) = 0 ↔ n = 0 := by + omega + +protected theorem natCast_ne_zero {n : Nat} : (n : Int) ≠ 0 ↔ n ≠ 0 := by + exact not_congr Int.natCast_eq_zero + +protected theorem gcd_def (i j : Int) : i.gcd j = i.natAbs.gcd j.natAbs := + rfl + +protected theorem gcd_def' (i : Int) (j : Nat) : i.gcd (ofNat j) = i.natAbs.gcd j := + Int.gcd_def _ _ + +theorem gcd_eq_zero_iff {i j : Int} : gcd i j = 0 ↔ i = 0 ∧ j = 0 := by + rw [gcd, Nat.gcd_eq_zero_iff, natAbs_eq_zero, natAbs_eq_zero] + +theorem gcd_ne_zero_iff {i j : Int} : gcd i j ≠ 0 ↔ i ≠ 0 ∨ j ≠ 0 := by + constructor + · intro h + let tmp := not_congr gcd_eq_zero_iff |>.mp h + if h_i : i = 0 then + simp [h_i] at tmp + exact Or.inr tmp + else + exact Or.inl h_i + · intro h gcd_zero + rw [gcd_eq_zero_iff] at gcd_zero + simp [gcd_zero.1, gcd_zero.2] at h + +protected theorem dvd_mul_left_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ k * j +| ⟨n, h⟩ => by + rw [h] + exists k * n + rw [ + ← Int.mul_assoc k i n, + Int.mul_comm k i, + Int.mul_assoc i k n, + ] + +protected theorem dvd_mul_right_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ j * k := + Int.mul_comm j k ▸ Int.dvd_mul_left_of_dvd k + +theorem flatten_div_mul_eq_mul_div + {i1 i2 i3 i4 j : Int} + (j_pos : j ≠ 0) + (j_dvd_i1 : j ∣ i1) + (j_dvd_i4 : j ∣ i4) +: i1 / j * i2 = i3 * (i4 / j) → i1 * i2 = i3 * i4 := by + intro h + rw [← Int.mul_eq_mul_left_iff j_pos] at h + conv at h => + lhs + rw [← Int.mul_assoc] + rw [← Int.mul_ediv_assoc _ j_dvd_i1] + rw [Int.mul_ediv_cancel_left _ j_pos] + conv at h => + rhs + rw [← Int.mul_assoc] + conv => lhs ; rw [Int.mul_comm] + rw [Int.mul_assoc] + rw [← Int.mul_ediv_assoc _ j_dvd_i4] + rw [Int.mul_ediv_cancel_left _ j_pos] + assumption + +theorem not_lt_of_lt_rev {i j : Int} : i < j → ¬ j < i := by + omega + +theorem lt_of_le_of_ne {i j : Int} : i ≤ j → i ≠ j → i < j := by + omega + +@[simp] +theorem zero_le_natCast {n : Nat} : (0 : Int) ≤ n := by omega + +@[simp] +theorem natCast_pos {n : Nat} : (0 : Int) < n ↔ 0 < n := by omega + +theorem div_nonneg_iff_of_pos' {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a := by + let tmp := @Int.div_nonneg_iff_of_pos a b h + simp [GE.ge] at tmp + exact tmp + +variable {a b c : Int} + +@[simp] protected +theorem neg_pos : 0 < -a ↔ a < 0 := ⟨Int.neg_of_neg_pos, Int.neg_pos_of_neg⟩ + +@[simp] protected +theorem neg_nonneg : 0 ≤ -a ↔ a ≤ 0 := ⟨Int.nonpos_of_neg_nonneg, Int.neg_nonneg_of_nonpos⟩ + +@[simp] protected +theorem neg_neg_iff_pos : -a < 0 ↔ 0 < a := ⟨Int.pos_of_neg_neg, Int.neg_neg_of_pos⟩ + +@[simp] protected +theorem neg_nonpos_iff_nonneg : -a ≤ 0 ↔ 0 ≤ a := + ⟨Int.nonneg_of_neg_nonpos, Int.neg_nonpos_of_nonneg⟩ + +@[simp] protected +theorem sub_pos : 0 < a - b ↔ b < a := ⟨Int.lt_of_sub_pos, Int.sub_pos_of_lt⟩ + +@[simp] protected +theorem sub_nonneg : 0 ≤ a - b ↔ b ≤ a := ⟨Int.le_of_sub_nonneg, Int.sub_nonneg_of_le⟩ + +protected theorem le_rfl : a ≤ a := a.le_refl +protected theorem lt_or_lt_of_ne : a ≠ b → a < b ∨ b < a := Int.lt_or_gt_of_ne +protected theorem lt_or_le (a b : Int) : a < b ∨ b ≤ a := by + rw [← Int.not_lt] + apply Decidable.em +protected theorem le_or_lt (a b : Int) : a ≤ b ∨ b < a := (b.lt_or_le a).symm +protected theorem lt_asymm : a < b → ¬ b < a := by rw [Int.not_lt]; exact Int.le_of_lt +protected theorem le_of_eq (hab : a = b) : a ≤ b := by rw [hab]; exact Int.le_rfl +protected theorem ge_of_eq (hab : a = b) : b ≤ a := Int.le_of_eq hab.symm +protected theorem le_antisymm_iff {a b : Int} : a = b ↔ a ≤ b ∧ b ≤ a := + ⟨fun h ↦ ⟨Int.le_of_eq h, Int.ge_of_eq h⟩, fun h ↦ Int.le_antisymm h.1 h.2⟩ +protected theorem le_iff_eq_or_lt {a b : Int} : a ≤ b ↔ a = b ∨ a < b := by + rw [Int.le_antisymm_iff, Int.lt_iff_le_not_le, ← and_or_left] + simp [Decidable.em] +protected theorem le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := by rw [Int.le_iff_eq_or_lt, or_comm] +end Int diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean index 91f2e218..d4640f63 100644 --- a/Smt/Reconstruct/Rat/Core.lean +++ b/Smt/Reconstruct/Rat/Core.lean @@ -5,78 +5,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ +import Batteries.Logic import Batteries.Data.Rat - -namespace Int -@[simp] -protected theorem natCast_eq_zero {n : Nat} : (n : Int) = 0 ↔ n = 0 := by - omega - -protected theorem natCast_ne_zero {n : Nat} : (n : Int) ≠ 0 ↔ n ≠ 0 := by - exact not_congr Int.natCast_eq_zero - -protected theorem gcd_def (i j : Int) : i.gcd j = i.natAbs.gcd j.natAbs := - rfl - -protected theorem gcd_def' (i : Int) (j : Nat) : i.gcd (ofNat j) = i.natAbs.gcd j := - Int.gcd_def _ _ - -theorem gcd_eq_zero_iff {i j : Int} : gcd i j = 0 ↔ i = 0 ∧ j = 0 := by - rw [gcd, Nat.gcd_eq_zero_iff, natAbs_eq_zero, natAbs_eq_zero] - -theorem gcd_ne_zero_iff {i j : Int} : gcd i j ≠ 0 ↔ i ≠ 0 ∨ j ≠ 0 := by - constructor - · intro h - let tmp := not_congr gcd_eq_zero_iff |>.mp h - if h_i : i = 0 then - simp [h_i] at tmp - exact Or.inr tmp - else - exact Or.inl h_i - · intro h gcd_zero - rw [gcd_eq_zero_iff] at gcd_zero - simp [gcd_zero.1, gcd_zero.2] at h - -protected theorem dvd_mul_left_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ k * j -| ⟨n, h⟩ => by - rw [h] - exists k * n - rw [ - ← Int.mul_assoc k i n, - Int.mul_comm k i, - Int.mul_assoc i k n, - ] - -protected theorem dvd_mul_right_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ j * k := - Int.mul_comm j k ▸ Int.dvd_mul_left_of_dvd k - -theorem flatten_div_mul_eq_mul_div - {i1 i2 i3 i4 j : Int} - (j_pos : j ≠ 0) - (j_dvd_i1 : j ∣ i1) - (j_dvd_i4 : j ∣ i4) -: i1 / j * i2 = i3 * (i4 / j) → i1 * i2 = i3 * i4 := by - intro h - rw [← Int.mul_eq_mul_left_iff j_pos] at h - conv at h => - lhs - rw [← Int.mul_assoc] - rw [← Int.mul_ediv_assoc _ j_dvd_i1] - rw [Int.mul_ediv_cancel_left _ j_pos] - conv at h => - rhs - rw [← Int.mul_assoc] - conv => lhs ; rw [Int.mul_comm] - rw [Int.mul_assoc] - rw [← Int.mul_ediv_assoc _ j_dvd_i4] - rw [Int.mul_ediv_cancel_left _ j_pos] - assumption -end Int +import Smt.Reconstruct.Int.Core namespace Rat +protected theorem lt_iff_blt {x y : Rat} : x < y ↔ x.blt y := by + simp only [LT.lt] theorem num_divInt_den (q : Rat) : q.num /. q.den = q := divInt_self _ @@ -174,4 +112,80 @@ protected theorem mul_assoc (a b c : Rat) : a + b + c = a + (b + c) := numDenCasesOn' c fun n₃ d₃ _h₃ => by simp only [Rat.divInt_ofNat] exact Rat.add_assoc _ _ _ + + + +@[simp] +theorem mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by + congr + + + +variable {q : Rat} + +@[simp] +theorem neg_neg : - -q = q := by + rw [← Rat.mkRat_self q] + simp [Rat.neg_mkRat] + +@[simp] +theorem num_eq_zero : q.num = 0 ↔ q = 0 := by + induction q + constructor + · rintro rfl + exact mk'_zero _ _ _ + · exact congr_arg num + +theorem num_ne_zero : q.num ≠ 0 ↔ q ≠ 0 := not_congr num_eq_zero + +@[simp] +theorem num_nonneg : 0 ≤ q.num ↔ 0 ≤ q := by + simp [Int.le_iff_lt_or_eq, instLE, Rat.blt, Int.not_lt] + omega + +theorem nonneg_iff_sub_nonpos : 0 ≤ q ↔ -q ≤ 0 := by + rw [← num_nonneg] + conv => rhs ; simp [LE.le, Rat.blt] + omega + +theorem nonneg_sub_iff_nonpos : 0 ≤ -q ↔ q ≤ 0 := by + simp [nonneg_iff_sub_nonpos, Rat.neg_neg] + + +@[simp] +theorem num_nonpos : q.num ≤ 0 ↔ q ≤ 0 := by + conv => lhs ; rw [← Int.neg_nonneg] + simp [Rat.neg_num q ▸ @num_nonneg (-q)] + conv => rhs ; rw [← nonneg_sub_iff_nonpos] + +theorem not_nonpos : ¬ q ≤ 0 ↔ 0 < q := by + simp [Rat.lt_iff_blt, Rat.blt] + rw [← num_nonpos] + exact Int.not_le + +@[simp] +theorem num_pos : 0 < q.num ↔ 0 < q := by + let tmp := not_congr (num_nonpos (q := q)) + rw [Int.not_le] at tmp + simp [tmp, Rat.not_nonpos] + +theorem pos_iff_neg_nonpos : 0 < q ↔ -q < 0 := by + rw [← num_pos] + conv => rhs ; simp [Rat.lt_iff_blt] ; unfold Rat.blt ; simp + constructor <;> intro h + · apply Or.inl + exact num_pos.mp h + · let h : 0 < q := by + cases h + case inl h => exact h + case inr h => exact h.2.2 + apply num_pos.mpr h + +@[simp] +theorem num_neg : q.num < 0 ↔ q < 0 := by + let tmp := @num_pos (-q) + simp [Rat.neg_num q, Int.lt_neg_of_lt_neg] at tmp + rw [tmp] + apply Rat.neg_neg ▸ Rat.pos_iff_neg_nonpos (q := -q) + end Rat From 86acef5f6d8de64c4db16ca368bdd16cc3bf93c1 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Thu, 20 Jun 2024 17:56:21 +0200 Subject: [PATCH 3/6] feat: `Rat.le_def` and `Rat.lt_def` --- Smt/Reconstruct/Int/Core.lean | 35 +++ Smt/Reconstruct/Rat/Core.lean | 364 ++++++++++++++++++++++++++++---- Smt/Reconstruct/Rat/Lemmas.lean | 67 +++++- 3 files changed, 419 insertions(+), 47 deletions(-) diff --git a/Smt/Reconstruct/Int/Core.lean b/Smt/Reconstruct/Int/Core.lean index 7b569139..27f1549b 100644 --- a/Smt/Reconstruct/Int/Core.lean +++ b/Smt/Reconstruct/Int/Core.lean @@ -86,6 +86,9 @@ theorem zero_le_natCast {n : Nat} : (0 : Int) ≤ n := by omega @[simp] theorem natCast_pos {n : Nat} : (0 : Int) < n ↔ 0 < n := by omega +@[simp] +theorem natCast_nonneg {n : Nat} : (0 : Int) ≤ n := by omega + theorem div_nonneg_iff_of_pos' {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a := by let tmp := @Int.div_nonneg_iff_of_pos a b h simp [GE.ge] at tmp @@ -127,4 +130,36 @@ protected theorem le_iff_eq_or_lt {a b : Int} : a ≤ b ↔ a = b ∨ a < b := b rw [Int.le_antisymm_iff, Int.lt_iff_le_not_le, ← and_or_left] simp [Decidable.em] protected theorem le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := by rw [Int.le_iff_eq_or_lt, or_comm] + + + +protected theorem div_gcd_nonneg_iff_of_pos + {b : Nat} (b_pos : 0 < b) +: 0 ≤ a / (a.gcd b) ↔ 0 ≤ a := by + let nz_den : (0 : Int) < a.gcd b := by + apply Int.natCast_pos.mpr + simp [Int.gcd] + apply Nat.gcd_pos_of_pos_right _ b_pos + exact Int.div_nonneg_iff_of_pos nz_den + +protected theorem div_gcd_nonneg_iff_of_nz + {b : Nat} (nz_b : b ≠ 0) +: 0 ≤ a / (a.gcd b) ↔ 0 ≤ a := + Nat.pos_of_ne_zero nz_b |> Int.div_gcd_nonneg_iff_of_pos + + +@[simp] +theorem mul_nonneg_iff_of_pos_right (c_pos : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b := ⟨ + by + intro bc_nonneg + apply Decidable.byContradiction + intro h_b + let h_b := Int.not_le.mp h_b + apply Int.not_le.mpr (Int.mul_neg_of_neg_of_pos h_b c_pos) + assumption + , + by + intro b_nonneg + apply Int.mul_nonneg b_nonneg (Int.le_of_lt c_pos) +⟩ end Int diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean index d4640f63..d442abc0 100644 --- a/Smt/Reconstruct/Rat/Core.lean +++ b/Smt/Reconstruct/Rat/Core.lean @@ -13,8 +13,9 @@ import Smt.Reconstruct.Int.Core namespace Rat -protected theorem lt_iff_blt {x y : Rat} : x < y ↔ x.blt y := by - simp only [LT.lt] + + +section basics theorem num_divInt_den (q : Rat) : q.num /. q.den = q := divInt_self _ @@ -42,9 +43,99 @@ def numDenCasesOn''.{u} {C : Rat → Sort u} (a : Rat) rw [← mk_eq_divInt _ _ h_pos h'] exact H n d h_pos _ +theorem normalize_eq_mk' + (n : Int) (d : Nat) (h : d ≠ 0) (c : Nat.gcd (Int.natAbs n) d = 1) +: normalize n d h = mk' n d h c := + (mk_eq_normalize ..).symm + +protected theorem normalize_den_ne_zero +: ∀ {d : Int} {n : Nat}, (h : n ≠ 0) → (normalize d n h).den ≠ 0 := by + intro d n nz + simp only [Rat.normalize_eq, ne_eq] + intro h + apply nz + rw [← Nat.zero_mul (d.natAbs.gcd n)] + apply Nat.div_eq_iff_eq_mul_left _ _ |>.mp + · assumption + · exact Nat.gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero nz) + · exact Nat.gcd_dvd_right _ _ + +protected theorem eq_mkRat : ∀ a : Rat, a = mkRat a.num a.den := fun a => by + simp [Rat.mkRat_def, a.den_nz, Rat.normalize_eq, a.reduced] + +@[simp] +theorem mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by + congr + +theorem eq_iff_mul_eq_mul {p q : Rat} : p = q ↔ p.num * q.den = q.num * p.den := by + conv => + lhs + rw [← num_divInt_den p, ← num_divInt_den q] + apply Rat.divInt_eq_iff <;> + · rw [← Int.natCast_zero, Ne, Int.ofNat_inj] + apply den_nz + +end basics + -protected theorem add_comm (a b : Rat) : a + b = b + a := by +section le_lt_basics + +protected theorem not_le {q' : Rat} : ¬q ≤ q' ↔ q' < q := by + exact (Bool.not_eq_false _).to_iff + +protected theorem not_lt {q' : Rat} : ¬q < q' ↔ q' ≤ q := by + rw [not_congr (Rat.not_le (q := q') (q' := q)) |>.symm] + simp only [Decidable.not_not] + +protected theorem lt_iff_blt {x y : Rat} : x < y ↔ x.blt y := by + simp only [LT.lt] + +protected theorem le_iff_blt {x y : Rat} : x ≤ y ↔ ¬ y.blt x := by + simp [LE.le] + +protected theorem lt_asymm {x y : Rat} : x < y → ¬ y < x := by + simp [Rat.lt_iff_blt] + simp [Rat.blt] + intro h + cases h with + | inl h => + simp [Int.not_lt_of_lt_rev h.1, Int.not_le.mpr h.1, Int.le_of_lt h.1] + intro nz_ynum ynum_neg _ + apply ynum_neg + apply Int.lt_of_le_of_ne h.2 + intro h + apply nz_ynum + rw [h] + | inr h => + split at h + case inl xnum_0 => + simp [Int.not_lt_of_lt_rev h, xnum_0, h] + case inr xnum_ne_0 => + let ⟨h, h'⟩ := h + simp [Int.not_lt_of_lt_rev h'] + cases h + case inl h => + simp [h] + intro _ xnum_pos + apply h + apply Int.lt_of_le_of_ne xnum_pos + intro eq ; apply xnum_ne_0 ; rw [eq] + case inr h => + simp [Int.not_le.mp h |> Int.not_lt_of_lt_rev] + intro eq + rw [eq] at h + contradiction + +end le_lt_basics + + + +section add_basics + +variable (a b c : Rat) + +protected theorem add_comm : a + b = b + a := by simp [add_def, Int.add_comm, Int.mul_comm, Nat.mul_comm] protected theorem add_zero : ∀ a : Rat, a + 0 = a @@ -52,14 +143,30 @@ protected theorem add_zero : ∀ a : Rat, a + 0 = a simp [Rat.add_def] simp only [Rat.normalize_eq_mkRat, Rat.mk_eq_normalize] -protected theorem zero_add : ∀ a : Rat, 0 + a = a := - fun a => Rat.add_comm a 0 ▸ Rat.add_zero a +protected theorem zero_add : 0 + a = a := + Rat.add_comm a 0 ▸ Rat.add_zero a -protected theorem eq_mkRat : ∀ a : Rat, a = mkRat a.num a.den := fun a => by - simp [Rat.mkRat_def, a.den_nz, Rat.normalize_eq, a.reduced] +protected theorem add_assoc : a + b + c = a + (b + c) := + numDenCasesOn' a fun n₁ d₁ h₁ => + numDenCasesOn' b fun n₂ d₂ h₂ => + numDenCasesOn' c fun n₃ d₃ h₃ => by + simp only [ + ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, + Rat.divInt_add_divInt, Int.mul_eq_zero, or_self, h₃ + ] + rw [Int.mul_assoc, Int.add_mul, Int.add_mul, Int.mul_assoc, Int.add_assoc] + congr 2 + ac_rfl + +end add_basics -protected theorem mul_eq_zero_iff : ∀ {a b : Rat}, a * b = 0 ↔ a = 0 ∨ b = 0 := by - intro a b + + +section mul_basics + +variable {a b : Rat} + +protected theorem mul_eq_zero_iff : a * b = 0 ↔ a = 0 ∨ b = 0 := by constructor · simp only [Rat.mul_def, Rat.normalize_eq_zero] intro h @@ -76,50 +183,21 @@ protected theorem mul_eq_zero_iff : ∀ {a b : Rat}, a * b = 0 ↔ a = 0 ∨ b = | .inl h => simp only [h, Rat.zero_mul] | .inr h => simp only [h, Rat.mul_zero] -protected theorem mul_ne_zero_iff : ∀ {a b : Rat}, a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by - intro a b +protected theorem mul_ne_zero_iff : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by simp only [not_congr (@Rat.mul_eq_zero_iff a b), not_or, ne_eq] -protected theorem normalize_den_ne_zero -: ∀ {d : Int} {n : Nat}, (h : n ≠ 0) → (normalize d n h).den ≠ 0 := by - intro d n nz - simp only [Rat.normalize_eq, ne_eq] - intro h - apply nz - rw [← Nat.zero_mul (d.natAbs.gcd n)] - apply Nat.div_eq_iff_eq_mul_left _ _ |>.mp - · assumption - · exact Nat.gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero nz) - · exact Nat.gcd_dvd_right _ _ - - - -protected theorem add_assoc (a b c : Rat) : a + b + c = a + (b + c) := - numDenCasesOn' a fun n₁ d₁ h₁ ↦ - numDenCasesOn' b fun n₂ d₂ h₂ ↦ - numDenCasesOn' c fun n₃ d₃ h₃ ↦ by - simp only [ - ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, - divInt_add_divInt, Int.mul_eq_zero, or_self, h₃ - ] - rw [Int.mul_assoc, Int.add_mul, Int.add_mul, Int.mul_assoc, Int.add_assoc] - congr 2 - ac_rfl - protected theorem mul_assoc (a b c : Rat) : a + b + c = a + (b + c) := numDenCasesOn' a fun n₁ d₁ _h₁ => - numDenCasesOn' b fun n₂ d₂ _h₂ => - numDenCasesOn' c fun n₃ d₃ _h₃ => by - simp only [Rat.divInt_ofNat] - exact Rat.add_assoc _ _ _ + numDenCasesOn' b fun n₂ d₂ _h₂ => + numDenCasesOn' c fun n₃ d₃ _h₃ => by + simp only [Rat.divInt_ofNat] + exact Rat.add_assoc _ _ _ +end mul_basics -@[simp] -theorem mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by - congr - +section num_related variable {q : Rat} @@ -188,4 +266,200 @@ theorem num_neg : q.num < 0 ↔ q < 0 := by rw [tmp] apply Rat.neg_neg ▸ Rat.pos_iff_neg_nonpos (q := -q) +@[simp] +theorem num_neg_eq_neg_num (q : Rat) : (-q).num = -q.num := + rfl + +end num_related + + + +section le_lt_extra + +variable {x y : Rat} + +protected theorem le_refl : x ≤ x := by + simp [Rat.le_iff_blt, Rat.blt] + if h : x = 0 then + simp [h] + rw [← Rat.num_neg, Rat.zero_num] + exact Int.lt_irrefl 0 + else + simp [h] + rw [← Rat.num_neg, ← Rat.num_pos] + omega + +protected theorem lt_irrefl : ¬ x < x := by + simp [Rat.not_lt, Rat.le_refl] + +protected theorem le_of_lt : x < y → x ≤ y := by + intro h_lt + apply Decidable.byContradiction + intro h + let _ := Rat.not_le.mp h + let _ := Rat.lt_asymm h_lt + contradiction + +protected theorem ne_of_lt : x < y → x ≠ y := by + intro h_lt h_eq + exact Rat.lt_irrefl (h_eq ▸ h_lt) + +end le_lt_extra + + + +section nonneg + +variable (x : Rat) + +protected theorem nonneg_total : 0 ≤ x ∨ 0 ≤ -x := by + rw [← num_nonneg (q := -x), ← num_nonneg (q := x)] + rw [Rat.neg_num, Int.neg_nonneg] + exact Int.le_total _ _ + +variable {x} + +protected theorem nonneg_antisymm : 0 ≤ x → 0 ≤ -x → x = 0 := by + rw [← Rat.num_eq_zero, ← Rat.num_nonneg, ← Rat.num_nonneg, Rat.num_neg_eq_neg_num] + omega + +end nonneg + + + +section neg_sub + +variable {x y : Rat} + +protected theorem neg_sub : -(x - y) = y - x := by + cases x with | mk' nx dx _ _ => + cases y with | mk' ny dy _ _ => + simp [Rat.sub_eq_add_neg, Neg.neg] + simp [Rat.neg, Rat.divInt_ofNat, Rat.add_def, Rat.normalize_eq] + rw [Nat.mul_comm dx dy] + constructor + · rw [← Int.neg_ediv_of_dvd] + rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.neg_sub] + rw [Int.neg_mul, ← Int.sub_eq_add_neg] + rw [← Int.natAbs_neg, Int.neg_sub] + · conv => lhs ; arg 1 ; arg 2 ; rw [← Int.natAbs_ofNat (dy * dx)] + exact Int.gcd_dvd_left + · rw [Int.neg_mul, ← Int.sub_eq_add_neg] + rw [Int.neg_mul, ← Int.sub_eq_add_neg] + rw [← Int.natAbs_neg, Int.neg_sub] + +@[simp] +protected theorem sub_self : x - x = 0 := + numDenCasesOn' x fun nx dx h_dx => by + rw [Rat.divInt_sub_divInt _ _ (Int.natCast_ne_zero.mpr h_dx) (Int.natCast_ne_zero.mpr h_dx)] + simp + +protected theorem add_neg_self : x + -x = 0 := + Rat.sub_eq_add_neg x x ▸ Rat.sub_self + +-- #TODO use `eq_iff_mul_eq_mul` +protected theorem eq_neg_of_add_eq_zero_left : x + y = 0 → x = - y := + numDenCasesOn'' x fun nx dx h_dx h_red => + numDenCasesOn'' y fun ny dy h_dy h_red' => by + simp only [Rat.neg_divInt, Rat.add_def] + intro h + simp [Neg.neg] ; simp [Rat.neg] + simp only [Rat.normalize_eq_zero] at h + let h_dpos : 0 < ↑dx := Int.natCast_pos.mpr (Nat.pos_iff_ne_zero.mpr h_dx) + let h_dpos' : 0 < ↑dy := Int.natCast_pos.mpr (Nat.pos_iff_ne_zero.mpr h_dy) + let h' := Int.neg_eq_of_add_eq_zero h + sorry + +protected theorem le_iff_sub_nonneg (x y : Rat) : x ≤ y ↔ 0 ≤ y - x := + numDenCasesOn'' x fun nx dx h_dx _ => + numDenCasesOn'' y fun ny dy h_dy _ => by + let dy_dx_nz : dy * dx ≠ 0 := + Nat.mul_ne_zero h_dy h_dx + change Rat.blt _ _ = false ↔ _ + unfold Rat.blt + simp only + [ Bool.and_eq_true, decide_eq_true_eq, Bool.ite_eq_false_distrib, + decide_eq_false_iff_not, Rat.not_lt, ite_eq_left_iff, + not_and, Rat.not_le, ← Rat.num_nonneg ] + if h : ny < 0 ∧ 0 ≤ nx then + simp [h] + simp only [Rat.sub_def, Rat.not_le, normalize_eq, Rat.neg] + simp [← Rat.num_neg] + apply Int.ediv_neg' + · apply Int.sub_neg_of_lt + apply Int.lt_of_lt_of_le (b := 0) + · apply Int.mul_neg_of_neg_of_pos h.1 + apply Int.natCast_pos.mpr + apply Nat.pos_of_ne_zero h_dx + · apply Int.mul_nonneg h.2 + exact Int.zero_le_natCast + · apply Int.natCast_pos.mpr + apply Nat.pos_iff_ne_zero.mpr + exact Nat.gcd_ne_zero_right dy_dx_nz + else + simp [h] + split + case inl nb_0 => + simp [nb_0, Rat.sub_eq_add_neg, Rat.zero_add, Rat.nonneg_sub_iff_nonpos, ← Rat.num_nonpos] + exact Int.not_lt + case inr nb_nz => + simp only [Rat.sub_def, normalize_eq, ← Rat.num_nonneg] + if ny_pos : 0 < ny then + simp [ny_pos] + if h_na : 0 < nx then + simp [Int.not_le.mpr h_na] + rw [Int.not_lt] + rw [← Int.sub_nonneg] + apply Iff.symm + apply Int.div_gcd_nonneg_iff_of_nz dy_dx_nz + else + let na_nonpos := Int.not_lt.mp h_na + simp [na_nonpos] + apply Int.div_gcd_nonneg_iff_of_nz dy_dx_nz |>.mpr + · apply Int.sub_nonneg_of_le + apply Int.le_trans (b := 0) + apply Int.mul_nonpos_of_nonpos_of_nonneg + · exact Int.not_lt.mp h_na + · exact Int.natCast_nonneg + · apply Int.mul_nonneg _ Int.natCast_nonneg + exact Int.le_of_lt ny_pos + else + simp [ny_pos, Int.not_lt, ← Int.sub_nonneg] + rw [Int.sub_zero] + rw [Int.sub_zero] + apply Iff.symm + apply Int.div_gcd_nonneg_iff_of_nz dy_dx_nz + +protected theorem sub_nonneg {a b : Rat} : 0 ≤ a - b ↔ b ≤ a := by + rw [Rat.le_iff_sub_nonneg b a] + +end neg_sub + + + +section divInt + +@[simp] +theorem divInt_nonneg_iff_of_pos_right {a b : Int} (hb : 0 < b) : 0 ≤ a /. b ↔ 0 ≤ a := by + cases hab : a /. b with | mk' n d hd hnd => + rw [mk'_eq_divInt, divInt_eq_iff (Int.ne_of_lt hb).symm (mod_cast hd)] at hab + rw [ + ← Rat.num_nonneg, ← Int.mul_nonneg_iff_of_pos_right hb, ← hab, + Int.mul_nonneg_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero hd), + ] + +protected theorem divInt_le_divInt + {a b c d : Int} (b0 : 0 < b) (d0 : 0 < d) +: a /. b ≤ c /. d ↔ a * d ≤ c * b := by + rw [Rat.le_iff_sub_nonneg, ← Int.sub_nonneg] + simp [Rat.sub_eq_add_neg, Rat.neg_divInt, Int.ne_of_gt b0, Int.ne_of_gt d0, Int.mul_pos d0 b0] + rw [Rat.divInt_add_divInt] + simp [Rat.divInt_nonneg_iff_of_pos_right (Int.mul_pos d0 b0)] + rw [← Int.sub_nonneg (a := c * b)] + rw [Int.neg_mul, ← Int.sub_eq_add_neg] + · apply Int.lt_iff_le_and_ne.mp d0 |>.2 |>.symm + · apply Int.lt_iff_le_and_ne.mp b0 |>.2 |>.symm + +end divInt + end Rat diff --git a/Smt/Reconstruct/Rat/Lemmas.lean b/Smt/Reconstruct/Rat/Lemmas.lean index 277da250..b71b5930 100644 --- a/Smt/Reconstruct/Rat/Lemmas.lean +++ b/Smt/Reconstruct/Rat/Lemmas.lean @@ -5,10 +5,73 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed -/ +import Batteries.Data.Int import Batteries.Data.Rat -private theorem Rat.mul_lt_mul_left {c x y : Rat} (hc : c > 0) : (c * x < c * y) = (x < y) := by - sorry +import Smt.Reconstruct.Int.Core +import Smt.Reconstruct.Rat.Core + + + +namespace Rat + + + +section le_lt_defs + +variable {x y : Rat} + +protected theorem le_antisymm (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by + rw [Rat.le_iff_sub_nonneg] at hxy hyx + rw [Rat.sub_eq_add_neg] at hyx + rw [← Rat.neg_sub, Rat.sub_eq_add_neg] at hxy + have this := Rat.eq_neg_of_add_eq_zero_left (Rat.nonneg_antisymm hyx hxy) + rwa [Rat.neg_neg] at this + +protected theorem le_def : x ≤ y ↔ x.num * y.den ≤ y.num * x.den := by + rw [← num_divInt_den y, ← num_divInt_den x] + conv => rhs ; simp only [num_divInt_den] + exact Rat.divInt_le_divInt (mod_cast x.den_pos) (mod_cast y.den_pos) + + +protected theorem le_total : x ≤ y ∨ y ≤ x := by + simp [Rat.le_def] + omega + +protected theorem lt_iff_le_not_le : x < y ↔ (x ≤ y ∧ ¬ y ≤ x) := by + rw [← Rat.not_le, and_iff_right_of_imp Rat.le_total.resolve_left] + +protected theorem lt_iff_le_and_ne : x < y ↔ x ≤ y ∧ x ≠ y := ⟨ + fun h => ⟨Rat.le_of_lt h, Rat.ne_of_lt h⟩, + fun h => by + let ⟨h_le, h_ne⟩ := h + rw [Rat.lt_iff_le_not_le] + apply And.intro h_le + intro h_le' + let _ := Rat.le_antisymm h_le h_le' + contradiction +⟩ + +protected theorem lt_def : x < y ↔ x.num * y.den < y.num * x.den := by + rw [Rat.lt_iff_le_and_ne, Rat.le_def] + suffices x ≠ y ↔ x.num * y.den ≠ y.num * x.den by + constructor <;> intro h + · exact Int.lt_iff_le_and_ne.mpr ⟨h.left, this.mp h.right⟩ + · have tmp := Int.lt_iff_le_and_ne.mp h + exact ⟨tmp.left, this.mpr tmp.right⟩ + exact Decidable.not_iff_not.mpr Rat.eq_iff_mul_eq_mul + +end le_lt_defs + +end Rat + + + +private theorem Rat.mul_lt_mul_left {c x y : Rat} : 0 < c → ((c * x < c * y) ↔ (x < y)) := + numDenCasesOn' x fun nx dx nz_dx => + numDenCasesOn' y fun ny dy nz_dy => + numDenCasesOn' c fun nc dc nz_dc => by + sorry private theorem Rat.mul_le_mul_left {c x y : Rat} (hc : c > 0) : (c * x ≤ c * y) = (x ≤ y) := by sorry From 02c0907c9bbd181977c37218e94c2b344e3d190f Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Mon, 8 Jul 2024 11:33:47 +0200 Subject: [PATCH 4/6] chore: proved `Rat.eq_neg_of_add_eq_zero_left` --- Smt/Reconstruct/Rat/Core.lean | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean index d442abc0..bce94b2a 100644 --- a/Smt/Reconstruct/Rat/Core.lean +++ b/Smt/Reconstruct/Rat/Core.lean @@ -66,6 +66,8 @@ protected theorem eq_mkRat : ∀ a : Rat, a = mkRat a.num a.den := fun a => by @[simp] theorem mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by congr + apply Nat.coprime_zero_left d |>.mp w + theorem eq_iff_mul_eq_mul {p q : Rat} : p = q ↔ p.num * q.den = q.num * p.den := by conv => @@ -109,7 +111,7 @@ protected theorem lt_asymm {x y : Rat} : x < y → ¬ y < x := by rw [h] | inr h => split at h - case inl xnum_0 => + case isTrue xnum_0 => simp [Int.not_lt_of_lt_rev h, xnum_0, h] case inr xnum_ne_0 => let ⟨h, h'⟩ := h @@ -357,18 +359,15 @@ protected theorem sub_self : x - x = 0 := protected theorem add_neg_self : x + -x = 0 := Rat.sub_eq_add_neg x x ▸ Rat.sub_self --- #TODO use `eq_iff_mul_eq_mul` protected theorem eq_neg_of_add_eq_zero_left : x + y = 0 → x = - y := - numDenCasesOn'' x fun nx dx h_dx h_red => - numDenCasesOn'' y fun ny dy h_dy h_red' => by - simp only [Rat.neg_divInt, Rat.add_def] + numDenCasesOn'' x fun nx dx h_dx h_dx_red => + numDenCasesOn'' y fun ny dy h_dy h_dy_red => by + simp only [Rat.neg_divInt, Rat.add_def, Neg.neg] + simp only [Rat.neg, normalize_eq_zero] + simp only [eq_iff_mul_eq_mul, ← Int.neg_mul_eq_neg_mul] intro h - simp [Neg.neg] ; simp [Rat.neg] - simp only [Rat.normalize_eq_zero] at h - let h_dpos : 0 < ↑dx := Int.natCast_pos.mpr (Nat.pos_iff_ne_zero.mpr h_dx) - let h_dpos' : 0 < ↑dy := Int.natCast_pos.mpr (Nat.pos_iff_ne_zero.mpr h_dy) - let h' := Int.neg_eq_of_add_eq_zero h - sorry + apply Int.eq_neg_of_eq_neg + exact Int.neg_eq_of_add_eq_zero h |>.symm protected theorem le_iff_sub_nonneg (x y : Rat) : x ≤ y ↔ 0 ≤ y - x := numDenCasesOn'' x fun nx dx h_dx _ => @@ -399,10 +398,10 @@ protected theorem le_iff_sub_nonneg (x y : Rat) : x ≤ y ↔ 0 ≤ y - x := else simp [h] split - case inl nb_0 => + case isTrue nb_0 => simp [nb_0, Rat.sub_eq_add_neg, Rat.zero_add, Rat.nonneg_sub_iff_nonpos, ← Rat.num_nonpos] exact Int.not_lt - case inr nb_nz => + case isFalse nb_nz => simp only [Rat.sub_def, normalize_eq, ← Rat.num_nonneg] if ny_pos : 0 < ny then simp [ny_pos] From 180678deeabc8fef9e9dd920a5352a35d95279f5 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Mon, 22 Jul 2024 16:38:50 +0200 Subject: [PATCH 5/6] chore: fix upstream merge --- Smt/Reconstruct/Rat.lean | 38 -------------------------------------- 1 file changed, 38 deletions(-) diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean index c0c84704..00449f92 100644 --- a/Smt/Reconstruct/Rat.lean +++ b/Smt/Reconstruct/Rat.lean @@ -347,39 +347,6 @@ where let c : Q(Rat) ← reconstructTerm pf.getResult[1]! let k₁ := pf.getChildren[0]!.getResult.getKind let k₂ := pf.getChildren[1]!.getResult.getKind -<<<<<<< HEAD - if k₁ == .GEQ && k₂ == .NOT then - let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! - let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! - addThm q($x > $c) q(Rat.trichotomy₁ $h₁ $h₂) - else if k₁ == .NOT && k₂ == .GEQ then - let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! - let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! - addThm q($x > $c) q(Rat.trichotomy₂ $h₁ $h₂) - else if k₁ == .GEQ && k₂ == .LEQ then - let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! - let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! - addThm q($x = $c) q(Rat.trichotomy₃ $h₁ $h₂) - else if k₁ == .LEQ && k₂ == .GEQ then - let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! - let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! - addThm q($x = $c) q(Rat.trichotomy₄ $h₁ $h₂) - else if k₁ == .NOT && k₂ == .LT then - let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! - let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! - addThm q($x < $c) q(Rat.trichotomy₅ $h₁ $h₂) - else if k₁ == .LT && k₂ == .NOT then - let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! - let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! - addThm q($x < $c) q(Rat.trichotomy₆ $h₁ $h₂) - else - return none - | .ARITH_POLY_NORM => - if pf.getResult[0]!.getSort.isInteger then return none - let a : Q(Rat) ← reconstructTerm pf.getResult[0]! - let b : Q(Rat) ← reconstructTerm pf.getResult[1]! - addTac q($a = $b) Rat.polyNorm -======= if k₁ == .LEQ && k₂ == .NOT then let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! @@ -440,7 +407,6 @@ where let a : Q(Int) ← reconstructTerm pf.getResult[0]! let b : Q(Int) ← reconstructTerm pf.getResult[1]! addTac q($a = $b) Rat.polyNorm ->>>>>>> upstream/main | .ARITH_MULT_SIGN => if pf.getResult[1]![0]!.getSort.isInteger then return none reconstructMulSign pf @@ -490,7 +456,3 @@ where | _ => return none end Smt.Reconstruct.Rat -<<<<<<< HEAD - -======= ->>>>>>> upstream/main From eb8dbc102095c3e5fc3c733c540a4a4181375cea Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Mon, 22 Jul 2024 16:40:09 +0200 Subject: [PATCH 6/6] feat: more useful Int/Rat lemmas --- Smt/Reconstruct/Int/Core.lean | 7 +++++++ Smt/Reconstruct/Rat/Core.lean | 20 ++++++++++++++++++++ 2 files changed, 27 insertions(+) diff --git a/Smt/Reconstruct/Int/Core.lean b/Smt/Reconstruct/Int/Core.lean index 27f1549b..e0b3395e 100644 --- a/Smt/Reconstruct/Int/Core.lean +++ b/Smt/Reconstruct/Int/Core.lean @@ -49,6 +49,13 @@ protected theorem dvd_mul_left_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ Int.mul_assoc i k n, ] +protected theorem natAbs_gcd_dvd {i : Int} {n : Nat} : ↑(i.natAbs.gcd n) ∣ i := by + refine ofNat_dvd_left.mpr ?_ + exact Nat.gcd_dvd_left _ _ + +protected theorem natAbs_gcd_dvd' (i : Int) (n : Nat) : ↑(i.natAbs.gcd n) ∣ i := + Int.natAbs_gcd_dvd + protected theorem dvd_mul_right_of_dvd {i j : Int} (k : Int) : i ∣ j → i ∣ j * k := Int.mul_comm j k ▸ Int.dvd_mul_left_of_dvd k diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean index bce94b2a..7a99eb1e 100644 --- a/Smt/Reconstruct/Rat/Core.lean +++ b/Smt/Reconstruct/Rat/Core.lean @@ -23,6 +23,26 @@ theorem num_divInt_den (q : Rat) : q.num /. q.den = q := theorem mk'_eq_divInt {n d h c} : (⟨n, d, h, c⟩ : Rat) = n /. d := (num_divInt_den _).symm +theorem divInt_num (q : Rat) : (q.num /. q.den).num = q.num := by + simp [mkRat, q.den_nz, normalize, Rat.reduced] + +theorem divInt_num' + {n : Int} {d : Nat} + (nz_d : d ≠ 0 := by omega) + (reduced : n.natAbs.Coprime d := by assumption) +: (n /. d).num = n := by + simp [mkRat, nz_d, normalize, reduced] + +theorem divInt_den (q : Rat) : (q.num /. q.den).den = q.den := by + simp [mkRat, q.den_nz, normalize, Rat.reduced] + +theorem divInt_den' + {n : Int} {d : Nat} + (nz_d : d ≠ 0 := by omega) + (reduced : n.natAbs.Coprime d := by assumption) +: (n /. d).den = d := by + simp [mkRat, nz_d, normalize, reduced] + @[elab_as_elim] def numDenCasesOn.{u} {C : Rat → Sort u} : ∀ (a : Rat) (_ : ∀ n d, 0 < d → (Int.natAbs n).Coprime d → C (n /. d)), C a