|
| 1 | +/- |
| 2 | +Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their |
| 3 | +institutional affiliations. All rights reserved. |
| 4 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 5 | +Authors: Abdalrhman Mohamed |
| 6 | +-/ |
| 7 | + |
| 8 | +import Lean |
| 9 | +import Smt.Preprocess.Basic |
| 10 | + |
| 11 | +namespace Smt.Preprocess |
| 12 | + |
| 13 | +theorem classical_ite_congr {α : Sort u} {c₁ c₂ : Prop} {h₁ : Decidable c₁} {t₁ t₂ e₁ e₂ : α} |
| 14 | + (hc : c₁ = c₂) (ht : t₁ = t₂) (he : e₁ = e₂) : |
| 15 | + @ite α c₁ h₁ t₁ e₁ = @ite α c₂ (Classical.propDecidable c₂) t₂ e₂ := by |
| 16 | + grind |
| 17 | + |
| 18 | +open Lean |
| 19 | + |
| 20 | +def replaceIteDecidableInst (e : Expr) : MetaM Expr := do |
| 21 | + go #[] e |
| 22 | +where |
| 23 | + go (xs : Array Expr) (e : Expr) : MetaM Expr := do |
| 24 | + match e with |
| 25 | + | mkApp3 (.const ``ite us) α c (.app (.const ``Classical.propDecidable []) _) => |
| 26 | + let α ← go xs α |
| 27 | + let c ← go xs c |
| 28 | + match ← Meta.synthInstance? (.app (.const ``Decidable []) (c.instantiateRev xs)) with |
| 29 | + | some h => return mkApp3 (.const ``ite us) α c h |
| 30 | + | none => return e |
| 31 | + | .app f a => |
| 32 | + let f ← go xs f |
| 33 | + let a ← go xs a |
| 34 | + return e.updateApp! f a |
| 35 | + | .lam n t b bi => |
| 36 | + let t ← go xs t |
| 37 | + Meta.withLocalDecl n bi (t.instantiateRev xs) fun x => do |
| 38 | + Meta.mkLambdaFVars #[x] (← go (xs.push x) b) false false false false |
| 39 | + | .forallE n t b bi => |
| 40 | + let t ← go xs t |
| 41 | + Meta.withLocalDecl n bi (t.instantiateRev xs) fun x => do |
| 42 | + Meta.mkForallFVars #[x] (← go (xs.push x) b) false false false |
| 43 | + | .letE n t v b nd => |
| 44 | + let t ← go xs t |
| 45 | + let v ← go xs v |
| 46 | + Meta.withLetDecl n t v (nondep := nd) fun x => do |
| 47 | + Meta.mkLetFVars #[x] (← go (xs.push x) b) false false |
| 48 | + | .proj _ _ b => |
| 49 | + return e.updateProj! (← go xs b) |
| 50 | + | .mdata _ a => |
| 51 | + return e.updateMData! (← go xs a) |
| 52 | + | _ => |
| 53 | + return e |
| 54 | + |
| 55 | +def mkEqIteDecidableInst (e : Expr) : MetaM Expr := do |
| 56 | + let e' ← replaceIteDecidableInst e |
| 57 | + Meta.mkAppM ``Eq #[e, e'] |
| 58 | + |
| 59 | +def containsClassicalPropDecidable (e : Expr) : Bool := |
| 60 | + (Expr.const ``Classical.propDecidable []).occurs e |
| 61 | + |
| 62 | +def replaceIteInst (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.withContext do |
| 63 | + let t ← instantiateMVars (← mv.getType) |
| 64 | + let ts ← hs.mapM (Meta.inferType · >>= instantiateMVars) |
| 65 | + if !(containsClassicalPropDecidable t || ts.any containsClassicalPropDecidable) then |
| 66 | + return { map := Std.HashMap.insertMany ∅ (hs.zip (hs.map .singleton)), hs, mv } |
| 67 | + let simpTheorems ← #[``eq_self, ``classical_ite_congr].foldlM (·.addConst ·) {} |
| 68 | + let simpTheorems := #[simpTheorems] |
| 69 | + let congrTheorems := {} |
| 70 | + let ctx ← Meta.Simp.mkContext {} simpTheorems congrTheorems |
| 71 | + let (hs', mv') ← replaceIteInstLocalDecls mv hs.toList ctx #[] |
| 72 | + let mv' ← replaceIteInstTarget mv' ctx |
| 73 | + return { map := Std.HashMap.insertMany ∅ (hs'.zip (hs.map .singleton)), hs := hs', mv := mv' } |
| 74 | +where |
| 75 | + replaceIteInstLocalDecls mv hs ctx hs' := do match hs with |
| 76 | + | [] => return (hs', mv) |
| 77 | + | h :: hs => |
| 78 | + let type ← Meta.inferType h |
| 79 | + let eq ← mkEqIteDecidableInst (← instantiateMVars type) |
| 80 | + let (_, l, r) := eq.eq?.get! |
| 81 | + if l == r then |
| 82 | + replaceIteInstLocalDecls mv hs ctx (hs'.push h) |
| 83 | + else |
| 84 | + let (res, _) ← Meta.simp eq ctx |
| 85 | + let h' := mkApp4 (.const ``Eq.mp [0]) l r (mkOfEqTrue eq (← res.getProof)) h |
| 86 | + if let .some fv := h.fvarId? then |
| 87 | + let res ← mv.replace fv h' (.some r) |
| 88 | + let hs' := hs'.map res.subst.apply |
| 89 | + let hs := hs.map res.subst.apply |
| 90 | + res.mvarId.withContext (replaceIteInstLocalDecls res.mvarId hs ctx (hs'.push (.fvar res.fvarId))) |
| 91 | + else |
| 92 | + replaceIteInstLocalDecls mv hs ctx (hs'.push h') |
| 93 | + termination_by hs.length |
| 94 | + replaceIteInstTarget mv ctx := mv.withContext do |
| 95 | + let eq ← mkEqIteDecidableInst (← instantiateMVars (← mv.getType)) |
| 96 | + let (res, _) ← Meta.simp eq ctx |
| 97 | + if res.expr.isTrue then |
| 98 | + mv.replaceTargetEq eq.appArg! (mkOfEqTrue eq (← res.getProof)) |
| 99 | + else |
| 100 | + return mv |
| 101 | + mkOfEqTrue p hpt := |
| 102 | + mkApp2 (.const ``of_eq_true []) p hpt |
| 103 | + |
| 104 | +end Smt.Preprocess |
| 105 | + |
| 106 | +syntax (name := replaceIteInst) "replace_ite_inst " "[" term,* "]" : tactic |
| 107 | + |
| 108 | +open Lean.Elab Tactic in |
| 109 | +@[tactic replaceIteInst] def evalReconstruct : Tactic |
| 110 | + | `(tactic| replace_ite_inst [$hs,*]) => withMainContext do |
| 111 | + let mv ← getMainGoal |
| 112 | + let hs ← hs.getElems.mapM (Term.elabTerm · none) |
| 113 | + Lean.logInfo m!"Before: {hs}" |
| 114 | + let ⟨_, hs, mv⟩ ← Smt.Preprocess.replaceIteInst mv hs |
| 115 | + mv.withContext (Lean.logInfo m!"After: {hs}") |
| 116 | + replaceMainGoal [mv] |
| 117 | + | _ => throwUnsupportedSyntax |
| 118 | + |
| 119 | +example (x : Int) : |
| 120 | + @ite Int (x > 0) (Classical.propDecidable (x > 0)) (x + 1) (x - 1) = |
| 121 | + @ite Int (x > 0) (Int.decLt 0 x) (x + 1) (x - 1) := by |
| 122 | + replace_ite_inst [] |
| 123 | + rfl |
| 124 | + |
| 125 | +example : |
| 126 | + (∀ x : Int, @ite Int (x > 0) (Classical.propDecidable (x > 0)) (x + 1) (x - 1) = 0) = |
| 127 | + (∀ x : Int, @ite Int (x > 0) (Int.decLt 0 x) (x + 1) (x - 1) = 0) := by |
| 128 | + replace_ite_inst [] |
| 129 | + rfl |
| 130 | + |
| 131 | +example (h : ∀ x : Int, @ite Int (x > 0) (Classical.propDecidable (x > 0)) (x + 1) (x - 1) = 0) |
| 132 | + : ∀ x : Int, @ite Int (x > 0) (Int.decLt 0 x) (x + 1) (x - 1) = 0 := by |
| 133 | + replace_ite_inst [h] |
| 134 | + exact h |
| 135 | + |
| 136 | +example (n : Int) : |
| 137 | + @ite Prop (@ite Prop (1 < n) (Classical.propDecidable _) False True) (Classical.propDecidable _) |
| 138 | + (@ite Prop (1 < n) (Classical.propDecidable _) False True) |
| 139 | + True = |
| 140 | + if if 1 < n then False else True then if 1 < n then False else True else True := by |
| 141 | + replace_ite_inst [] |
| 142 | + rfl |
| 143 | + |
| 144 | +open Smt.Preprocess |
| 145 | + |
| 146 | +set_option trace.Meta.Tactic.simp true |
| 147 | +set_option trace.Meta.Tactic.simp.congr true |
| 148 | + |
| 149 | +example (n : Int) : |
| 150 | + @ite Prop (@ite Prop (1 < n) (Classical.propDecidable _) False True) (Classical.propDecidable _) |
| 151 | + (@ite Prop (1 < n) (Classical.propDecidable _) False True) |
| 152 | + True = |
| 153 | + if if 1 < n then False else True then if 1 < n then False else True else True := by |
| 154 | + simp only [classical_ite_congr] |
| 155 | + |
| 156 | +example (x : Int) : |
| 157 | + @ite Int (x > 0) (Classical.propDecidable (x > 0)) (x + 1) (x - 1) = |
| 158 | + @ite Int (x > 0) (Int.decLt 0 x) (x + 1) (x - 1) := by |
| 159 | + simp only [classical_ite_congr] |
0 commit comments