diff --git a/SSA/Core/HVector.lean b/SSA/Core/HVector.lean index 30ff778f0..a3f88de41 100644 --- a/SSA/Core/HVector.lean +++ b/SSA/Core/HVector.lean @@ -116,7 +116,9 @@ theorem eq_of_type_eq_nil {A : α → Type*} {l : List α} syntax "[" withoutPosition(term,*) "]ₕ" : term @[simp] -theorem cons_nil_get : (HVector.cons x .nil).get (0 : Fin 1) = x := rfl +theorem cons_get_zero {A : α → Type*} {a: α} {as : List α} {e : A a} {vec : HVector A as} : + (HVector.cons e vec).get (@OfNat.ofNat (Fin (as.length + 1)) 0 Fin.instOfNat) = e := by + rfl -- Copied from core for List macro_rules diff --git a/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean b/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean index 39b9883a8..4e2cf97da 100644 --- a/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean +++ b/SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean @@ -253,7 +253,7 @@ def or : FSM Bool := (Circuit.var true (inr false))) Empty.elim } @[simp] lemma eval_or (x : Bool → BitStream) : or.eval x = (x true) ||| (x false) := by - ext n; cases n <;> simp [and, eval, nextBit] + ext n; cases n <;> simp [or, eval, nextBit] def xor : FSM Bool := { α := Empty, @@ -264,7 +264,7 @@ def xor : FSM Bool := (Circuit.var true (inr false))) Empty.elim } @[simp] lemma eval_xor (x : Bool → BitStream) : xor.eval x = (x true) ^^^ (x false) := by - ext n; cases n <;> simp [and, eval, nextBit] + ext n; cases n <;> simp [xor, eval, nextBit] def add : FSM Bool := { α := Unit, @@ -279,6 +279,13 @@ def add : FSM Bool := Circuit.var true (inr false) ^^^ Circuit.var true (inl ()) } +private theorem add_nextBitCirc_some_eval : + (add.nextBitCirc (some ())).eval = + fun x => x (inr true) && x (inr false) || x (inr true) + && x (inl ()) || x (inr false) && x (inl ()) := by + ext x + simp [add] + /-- The internal carry state of the `add` FSM agrees with the carry bit of addition as implemented on bitstreams -/ theorem carry_add_succ (x : Bool → BitStream) (n : ℕ) : @@ -290,7 +297,7 @@ theorem carry_add_succ (x : Bool → BitStream) (n : ℕ) : simp [carry, BitStream.addAux, nextBit, add, BitVec.adcb] | succ n ih => unfold carry - simp [nextBit, ih, Circuit.eval, BitStream.addAux, BitVec.adcb] + simp [add_nextBitCirc_some_eval, nextBit, ih, Circuit.eval, BitStream.addAux, BitVec.adcb, nextBitCirc, Sum.elim] @[simp] theorem carry_zero (x : ar → BitStream) : carry p x 0 = p.initCarry := rfl @[simp] theorem initCarry_add : add.initCarry = (fun _ => false) := rfl @@ -395,7 +402,7 @@ def one : FSM (Fin 0) := ext n cases n · rfl - · simp [eval, carry_one, nextBit] + · simp! [eval, carry_one, nextBit, one, mk] def negOne : FSM (Fin 0) := { α := Empty, @@ -427,7 +434,7 @@ theorem carry_ls (b : Bool) (x : Unit → BitStream) : ∀ (n : ℕ), ext n cases n · rfl - · simp [carry_ls, eval, nextBit, BitStream.concat] + · simp [ls, carry, carry_ls, eval, nextBit, BitStream.concat] def var (n : ℕ) : FSM (Fin (n+1)) := { α := Empty, diff --git a/SSA/Experimental/Bits/Fast/Circuit.lean b/SSA/Experimental/Bits/Fast/Circuit.lean index f13f31c59..32f6fc586 100644 --- a/SSA/Experimental/Bits/Fast/Circuit.lean +++ b/SSA/Experimental/Bits/Fast/Circuit.lean @@ -120,11 +120,12 @@ instance : AndOp (Circuit α) := ⟨Circuit.simplifyAnd⟩ @[simp] lemma eval_and : ∀ (c₁ c₂ : Circuit α) (f : α → Bool), (eval (c₁ &&& c₂) f) = ((eval c₁ f) && (eval c₂ f)) := by intros c₁ c₂ f - cases c₁ <;> cases c₂ <;> simp [eval, simplifyAnd] + cases c₁ <;> cases c₂ <;> simp [simplifyAnd, AndOp.and, HAnd.hAnd] theorem varsFinset_and [DecidableEq α] (c₁ c₂ : Circuit α) : (varsFinset (c₁ &&& c₂)) ⊆ (varsFinset c₁ ∪ varsFinset c₂) := by - cases c₁ <;> cases c₂ <;> simp [vars, simplifyAnd, varsFinset, Finset.subset_iff] + cases c₁ <;> cases c₂ <;> simp [vars, simplifyAnd, varsFinset, Finset.subset_iff, + AndOp.and, HAnd.hAnd] def simplifyOr : Circuit α → Circuit α → Circuit α | tru, _ => tru @@ -138,15 +139,18 @@ instance : OrOp (Circuit α) := ⟨Circuit.simplifyOr⟩ @[simp] lemma eval_or : ∀ (c₁ c₂ : Circuit α) (f : α → Bool), (eval (c₁ ||| c₂) f) = ((eval c₁ f) || (eval c₂ f)) := by intros c₁ c₂ f - cases c₁ <;> cases c₂ <;> simp [Circuit.simplifyOr, eval] + cases c₁ <;> cases c₂ <;> simp [Circuit.simplifyOr, eval, + OrOp.or, HOr.hOr] theorem vars_or [DecidableEq α] (c₁ c₂ : Circuit α) : (vars (c₁ ||| c₂)) ⊆ (vars c₁ ++ vars c₂).dedup := by - cases c₁ <;> cases c₂ <;> simp [vars, simplifyOr] + cases c₁ <;> cases c₂ <;> simp [vars, simplifyOr, + OrOp.or, HOr.hOr] theorem varsFinset_or [DecidableEq α] (c₁ c₂ : Circuit α) : (varsFinset (c₁ ||| c₂)) ⊆ (varsFinset c₁ ∪ varsFinset c₂) := by - cases c₁ <;> cases c₂ <;> simp [vars, simplifyOr, varsFinset, Finset.subset_iff] + cases c₁ <;> cases c₂ <;> simp [vars, simplifyOr, varsFinset, Finset.subset_iff, + OrOp.or, HOr.hOr] def simplifyNot : Circuit α → Circuit α | tru => fals @@ -173,13 +177,14 @@ theorem simplifyNot_eq_complement (c : Circuit α) : erw [eval, eval, eval_complement a, eval_complement b, Bool.not_and] | or a b, f => by erw [eval, eval, eval_complement a, eval_complement b, Bool.not_or] - | var true a, f => by simp [eval] - | var false a, f => by simp [eval] + | var true a, f => by simp [eval, ←simplifyNot_eq_complement, simplifyNot] + | var false a, f => by simp [eval, ←simplifyNot_eq_complement, simplifyNot] theorem varsFinset_complement [DecidableEq α] (c : Circuit α) : (varsFinset (~~~ c)) ⊆ varsFinset c := by intro x - induction c <;> simp [simplifyNot, vars, mem_varsFinset] <;> aesop + induction c <;> simp [simplifyNot, ←simplifyNot_eq_complement, vars, mem_varsFinset] + <;> aesop @[simp] def simplifyXor : Circuit α → Circuit α → Circuit α @@ -198,16 +203,15 @@ instance : Xor (Circuit α) := ⟨Circuit.simplifyXor⟩ @[simp] lemma eval_xor : ∀ (c₁ c₂ : Circuit α) (f : α → Bool), eval (c₁ ^^^ c₂) f = Bool.xor (eval c₁ f) (eval c₂ f) := by intros c₁ c₂ f - cases c₁ <;> cases c₂ <;> simp [simplifyXor, Bool.xor_not_left'] <;> - split_ifs <;> simp [*] at * + cases c₁ <;> cases c₂ <;> simp [simplifyXor, Bool.xor_not_left', HXor.hXor, Xor.xor] set_option maxHeartbeats 1000000 theorem vars_simplifyXor [DecidableEq α] (c₁ c₂ : Circuit α) : (vars (simplifyXor c₁ c₂)) ⊆ (vars c₁ ++ vars c₂).dedup := by intro x - simp only [List.mem_dedup, List.mem_append] + simp only [List.mem_dedup, List.mem_append, ←simplifyNot_eq_complement] induction c₁ <;> induction c₂ <;> simp only [simplifyXor, vars, - ← simplifyNot_eq_complement] at * <;> aesop + ← simplifyNot_eq_complement, simplifyNot] at * <;> aesop theorem varsFinset_simplifyXor [DecidableEq α] (c₁ c₂ : Circuit α) : (varsFinset (simplifyXor c₁ c₂)) ⊆ (varsFinset c₁ ∪ varsFinset c₂) := by diff --git a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean index 668c61c9c..cdd7e78e8 100644 --- a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean +++ b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean @@ -244,7 +244,7 @@ def or : FSM Bool := (Circuit.var true (inr false))) Empty.elim } @[simp] lemma eval_or (x : Bool → BitStream) : or.eval x = (x true) ||| (x false) := by - ext n; cases n <;> simp [and, eval, nextBit] + ext n; cases n <;> simp [or, eval, nextBit] def xor : FSM Bool := { α := Empty, @@ -334,7 +334,7 @@ lemma eval_scanAnd_succ (x : Unit → BitStream) (n : Nat) : exact h j (by omega) @[simp] lemma eval_xor (x : Bool → BitStream) : xor.eval x = (x true) ^^^ (x false) := by - ext n; cases n <;> simp [and, eval, nextBit] + ext n; cases n <;> simp [xor, eval, nextBit] @[simp] lemma eval_nxor (x : Bool → BitStream) : nxor.eval x = ((x true).nxor (x false)) := by ext n; cases n @@ -407,6 +407,13 @@ def add : FSM Bool := Circuit.var true (inr false) ^^^ Circuit.var true (inl ()) } +theorem add_nextBitCirc_some_eval : + (add.nextBitCirc (some ())).eval = + fun x => x (inr true) && x (inr false) || x (inr true) + && x (inl ()) || x (inr false) && x (inl ()) := by + ext x + simp +ground [eval, add, Circuit.simplifyAnd, Circuit.simplifyOr] + /-- The internal carry state of the `add` FSM agrees with the carry bit of addition as implemented on bitstreams -/ theorem carry_add_succ (x : Bool → BitStream) (n : ℕ) : @@ -418,7 +425,7 @@ theorem carry_add_succ (x : Bool → BitStream) (n : ℕ) : simp [carry, BitStream.addAux, nextBit, add, BitVec.adcb] | succ n ih => unfold carry - simp [nextBit, ih, Circuit.eval, BitStream.addAux, BitVec.adcb] + simp [add_nextBitCirc_some_eval, nextBit, ih, Circuit.eval, BitStream.addAux, BitVec.adcb] @[simp] theorem carry_zero (x : arity → BitStream) : carry p x 0 = p.initCarry := rfl @[simp] theorem initCarry_add : add.initCarry = (fun _ => false) := rfl @@ -558,7 +565,7 @@ def one : FSM (Fin 0) := ext n cases n · rfl - · simp [eval, carry_one, nextBit] + · simp! [eval, carry_one, nextBit, one] def negOne : FSM (Fin 0) := { α := Empty, @@ -593,7 +600,7 @@ theorem carry_ls (b : Bool) (x : Unit → BitStream) : ∀ (n : ℕ), ext n cases n · rfl - · simp [carry_ls, eval, nextBit, BitStream.concat] + · simp [ls, carry_ls, eval, nextBit, BitStream.concat, carry] def var (n : ℕ) : FSM (Fin (n+1)) := { α := Empty, diff --git a/SSA/Projects/CIRCT/DC/DC.lean b/SSA/Projects/CIRCT/DC/DC.lean index ce3c33a95..699a31628 100644 --- a/SSA/Projects/CIRCT/DC/DC.lean +++ b/SSA/Projects/CIRCT/DC/DC.lean @@ -186,19 +186,19 @@ instance : DialectSignature DC := ⟨Op.signature⟩ @[simp] instance : DialectDenote (DC) where denote - | .fst, arg, _ => (arg.getN 0).fst - | .snd, arg, _ => (arg.getN 0).snd - | .fstVal _, arg, _ => (arg.getN 0).fst - | .sndVal _, arg, _ => (arg.getN 0).snd - | .pair _, arg, _ => (arg.getN 0, arg.getN 1) - | .unpack _, arg, _ => CIRCTStream.DC.unpack (arg.getN 0) - | .pack _, arg, _ => CIRCTStream.DC.pack (arg.getN 0) (arg.getN 1) - | .branch, arg, _ => CIRCTStream.DC.branch (arg.getN 0) - | .fork, arg, _ => CIRCTStream.DC.fork (arg.getN 0) - | .join, arg, _ => CIRCTStream.DC.join (arg.getN 0) (arg.getN 1) - | .merge, arg, _ => CIRCTStream.DC.merge (arg.getN 0) (arg.getN 1) - | .select, arg, _ => CIRCTStream.DC.select (arg.getN 0) (arg.getN 1) (arg.getN 2) - | .sink, arg, _ => CIRCTStream.DC.sink (arg.getN 0) + | .fst, arg, _ => (arg.getN 0 (by simp [DialectSignature.sig, signature])).fst + | .snd, arg, _ => (arg.getN 0 (by simp [DialectSignature.sig, signature])).snd + | .fstVal _, arg, _ => (arg.getN 0 (by simp [DialectSignature.sig, signature])).fst + | .sndVal _, arg, _ => (arg.getN 0 (by simp [DialectSignature.sig, signature]) ).snd + | .pair _, arg, _ => (arg.getN 0 (by simp [DialectSignature.sig, signature]), arg.getN 1 (by simp [DialectSignature.sig, signature])) + | .unpack _, arg, _ => CIRCTStream.DC.unpack (arg.getN 0 (by simp [DialectSignature.sig, signature])) + | .pack _, arg, _ => CIRCTStream.DC.pack (arg.getN 0 (by simp [DialectSignature.sig, signature])) (arg.getN 1 (by simp [DialectSignature.sig, signature])) + | .branch, arg, _ => CIRCTStream.DC.branch (arg.getN 0 (by simp [DialectSignature.sig, signature])) + | .fork, arg, _ => CIRCTStream.DC.fork (arg.getN 0 (by simp [DialectSignature.sig, signature])) + | .join, arg, _ => CIRCTStream.DC.join (arg.getN 0 (by simp [DialectSignature.sig, signature])) (arg.getN 1 (by simp [DialectSignature.sig, signature])) + | .merge, arg, _ => CIRCTStream.DC.merge (arg.getN 0 (by simp [DialectSignature.sig, signature])) (arg.getN 1 (by simp [DialectSignature.sig, signature])) + | .select, arg, _ => CIRCTStream.DC.select (arg.getN 0 (by simp [DialectSignature.sig, signature])) (arg.getN 1 (by simp [DialectSignature.sig, signature])) (arg.getN 2 (by simp [DialectSignature.sig, signature])) + | .sink, arg, _ => CIRCTStream.DC.sink (arg.getN 0 (by simp [DialectSignature.sig, signature])) | .source, _, _ => CIRCTStream.DC.source end Dialect diff --git a/SSA/Projects/CIRCT/Handshake/Handshake.lean b/SSA/Projects/CIRCT/Handshake/Handshake.lean index 39aa1fb67..8ab0b2482 100644 --- a/SSA/Projects/CIRCT/Handshake/Handshake.lean +++ b/SSA/Projects/CIRCT/Handshake/Handshake.lean @@ -246,10 +246,10 @@ instance : DialectSignature Handshake := ⟨Op.signature⟩ @[simp] instance : DialectDenote (Handshake) where denote - | .branch _, arg, _ => CIRCTStream.Handshake.branch (arg.getN 0) (arg.getN 1) - | .merge _, arg, _ => CIRCTStream.Handshake.merge (arg.getN 0) (arg.getN 1) - | .fst _, arg, _ => (arg.getN 0).fst - | .snd _, arg, _ => (arg.getN 0).snd + | .branch _, arg, _ => CIRCTStream.Handshake.branch (arg.getN 0 (by simp [DialectSignature.sig, signature])) (arg.getN 1 (by simp [DialectSignature.sig, signature])) + | .merge _, arg, _ => CIRCTStream.Handshake.merge (arg.getN 0 (by simp [DialectSignature.sig, signature])) (arg.getN 1 (by simp [DialectSignature.sig, signature])) + | .fst _, arg, _ => (arg.getN 0 (by simp [DialectSignature.sig, signature])).fst + | .snd _, arg, _ => (arg.getN 0 (by simp [DialectSignature.sig, signature])).snd end Dialect diff --git a/SSA/Projects/InstCombine/Base.lean b/SSA/Projects/InstCombine/Base.lean index dfeaf329f..ed8b0cb53 100644 --- a/SSA/Projects/InstCombine/Base.lean +++ b/SSA/Projects/InstCombine/Base.lean @@ -381,27 +381,27 @@ def Op.denote (o : LLVM.Op) (op : HVector TyDenote.toType (DialectSignature.sig (TyDenote.toType <| DialectSignature.outTy o) := match o with | Op.const _ val => const? _ val - | Op.copy _ => (op.getN 0) - | Op.not _ => LLVM.not (op.getN 0) - | Op.neg _ => LLVM.neg (op.getN 0) - | Op.trunc w w' flags => LLVM.trunc w' (op.getN 0) flags - | Op.zext w w' flag => LLVM.zext w' (op.getN 0) flag - | Op.sext w w' => LLVM.sext w' (op.getN 0) - | Op.and _ => LLVM.and (op.getN 0) (op.getN 1) - | Op.or _ flag => LLVM.or (op.getN 0) (op.getN 1) flag - | Op.xor _ => LLVM.xor (op.getN 0) (op.getN 1) - | Op.shl _ flags => LLVM.shl (op.getN 0) (op.getN 1) flags - | Op.lshr _ flag => LLVM.lshr (op.getN 0) (op.getN 1) flag - | Op.ashr _ flag => LLVM.ashr (op.getN 0) (op.getN 1) flag - | Op.sub _ flags => LLVM.sub (op.getN 0) (op.getN 1) flags - | Op.add _ flags => LLVM.add (op.getN 0) (op.getN 1) flags - | Op.mul _ flags => LLVM.mul (op.getN 0) (op.getN 1) flags - | Op.sdiv _ flag => LLVM.sdiv (op.getN 0) (op.getN 1) flag - | Op.udiv _ flag => LLVM.udiv (op.getN 0) (op.getN 1) flag - | Op.urem _ => LLVM.urem (op.getN 0) (op.getN 1) - | Op.srem _ => LLVM.srem (op.getN 0) (op.getN 1) - | Op.icmp c _ => LLVM.icmp c (op.getN 0) (op.getN 1) - | Op.select _ => LLVM.select (op.getN 0) (op.getN 1) (op.getN 2) + | Op.copy _ => (op.getN 0 (by simp [DialectSignature.sig, signature])) + | Op.not _ => LLVM.not (op.getN 0 (by simp [DialectSignature.sig, signature])) + | Op.neg _ => LLVM.neg (op.getN 0 (by simp [DialectSignature.sig, signature])) + | Op.trunc w w' flags => LLVM.trunc w' (op.getN 0 (by simp [DialectSignature.sig, signature])) flags + | Op.zext w w' flag => LLVM.zext w' (op.getN 0 (by simp [DialectSignature.sig, signature])) flag + | Op.sext w w' => LLVM.sext w' (op.getN 0 (by simp [DialectSignature.sig, signature])) + | Op.and _ => LLVM.and (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) + | Op.or _ flag => LLVM.or (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flag + | Op.xor _ => LLVM.xor (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) + | Op.shl _ flags => LLVM.shl (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flags + | Op.lshr _ flag => LLVM.lshr (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flag + | Op.ashr _ flag => LLVM.ashr (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flag + | Op.sub _ flags => LLVM.sub (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flags + | Op.add _ flags => LLVM.add (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flags + | Op.mul _ flags => LLVM.mul (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flags + | Op.sdiv _ flag => LLVM.sdiv (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flag + | Op.udiv _ flag => LLVM.udiv (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) flag + | Op.urem _ => LLVM.urem (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) + | Op.srem _ => LLVM.srem (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) + | Op.icmp c _ => LLVM.icmp c (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) + | Op.select _ => LLVM.select (op.getN 0 (by simp [DialectSignature.sig, signature])) (op.getN 1 (by simp [DialectSignature.sig, signature])) (op.getN 2 (by simp [DialectSignature.sig, signature])) instance : DialectDenote LLVM := ⟨ fun o args _ => Op.denote o args diff --git a/SSA/Projects/InstCombine/LLVM/PrettyEDSL.lean b/SSA/Projects/InstCombine/LLVM/PrettyEDSL.lean index 7541a9139..408b1b852 100644 --- a/SSA/Projects/InstCombine/LLVM/PrettyEDSL.lean +++ b/SSA/Projects/InstCombine/LLVM/PrettyEDSL.lean @@ -241,7 +241,7 @@ private def pretty_test_exact := example : pretty_test = prettier_test_generic 32 := by unfold pretty_test prettier_test_generic simp_alive_meta - simp + rfl example : pretty_test_generic = prettier_test_generic := rfl diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 444b8e5e4..10c7e39e5 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -17,40 +17,40 @@ and all `Width.mvar` should be resolved into `Width.concrete`. -/ macro "simp_alive_meta" : tactic => `(tactic| ( - simp (config := {failIfUnchanged := false }) only [Com.changeDialect_ret, + try simp (config := {failIfUnchanged := false }) only [Com.changeDialect_ret, Com.changeDialect_var, Expr.changeDialect] - simp (config := {failIfUnchanged := false }) only [(HVector.changeDialect_nil)] - dsimp (config := {failIfUnchanged := false }) only [HVector.map'] - dsimp (config := {failIfUnchanged := false }) only [Functor.map] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.succ_eq_toSnoc] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.zero_eq_last] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.DerivedCtxt.snoc_ctxt_eq_ctxt_snoc] - dsimp (config := {failIfUnchanged := false }) only [List.map] - dsimp (config := {failIfUnchanged := false }) only [Width.mvar] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_snoc, Ctxt.map_nil] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.get?] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.map, Ctxt.snoc] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toSnoc_toMap] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_cons] - dsimp (config := {failIfUnchanged := false }) only + try simp (config := {failIfUnchanged := false }) only [(HVector.changeDialect_nil)] + try simp (config := {failIfUnchanged := false }) only [HVector.map'] + try dsimp (config := {failIfUnchanged := false }) only [Functor.map] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.succ_eq_toSnoc] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.zero_eq_last] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.DerivedCtxt.snoc_ctxt_eq_ctxt_snoc] + try dsimp (config := {failIfUnchanged := false }) only [List.map] + try dsimp (config := {failIfUnchanged := false }) only [Width.mvar] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_snoc, Ctxt.map_nil] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.get?] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.map, Ctxt.snoc] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toSnoc_toMap] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] + try dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_cons] + try dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.MOp.instantiateCom] - dsimp (config := {failIfUnchanged := false }) only + try dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMTy] - dsimp (config := {failIfUnchanged := false }) only [Fin.zero_eta, List.map_cons] - dsimp (config := {failIfUnchanged := false }) only + try dsimp (config := {failIfUnchanged := false }) only [Fin.zero_eta, List.map_cons] + try dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMOp] - dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero] - dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero'] - dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero''] - dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate] - dsimp (config := {failIfUnchanged := false }) only + try dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero] + try dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero'] + try dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero''] + try dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate] + try dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMTy] - dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero''] + try dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero''] -- How can I avoid this `simp! only` and instead use a plain `simp only`? - dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.ofNat_eq_concrete] - simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_ofNat_eq] + try dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.ofNat_eq_concrete] + try simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_ofNat_eq] ) ) @@ -70,7 +70,7 @@ macro "simp_alive_ssa" : tactic => simp (config := {failIfUnchanged := false}) only [ InstCombine.Op.denote, HVector.getN, HVector.get, - beq_self_eq_true, Option.isSome_some, HVector.cons_nil_get + beq_self_eq_true, Option.isSome_some, HVector.cons_get_zero ] -- Fold integers into their canonical form. diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 98a329d17..0d2eb1c83 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -235,7 +235,7 @@ def bb0IcomGeneric (w : Nat) := [llvm(w)| example : bb0IcomGeneric 32 = bb0IcomConcrete := by unfold bb0IcomGeneric bb0IcomConcrete simp_alive_meta - simp + rfl /- Simple example of the denotation of `GenericWidth`. diff --git a/lake-manifest.json b/lake-manifest.json index 159482c91..69ef6b92e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8a4877456aa721f76724451be03284db54851891", + "rev": "b774a65bf5d20fd92d63eb98d03be2b29dfd9f27", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-12-20", + "inputRev": "nightly-testing-2024-12-21", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2e82cd8e5d6462f20ffd810ea0e9460475e0b455", + "rev": "1a278069eda32a2dc0ce4d59eeb77d318373d10e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index 4ddae2c77..6a5d25e0d 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["SSA"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "nightly-testing-2024-12-20" +rev = "nightly-testing-2024-12-21" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index bba519d51..7b8b74ec5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-20 +leanprover/lean4:nightly-2024-12-21