internlm/Lean-Github huggingface dataset:
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
case nil

⊢ logic1 (fun x => !x) nil = logic2 (fun x x_1 => x != x_1) nil nil
Tactic:
simp
Proof state after:
no goals
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n (I minusOne)
Tactic:
match n with
| .I m => simp [logic1, logic2, ih]
| .O m => simp [logic1, logic2, ih]
Proof state after:
no goals
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
m : FinInt sz
⊢ logic1 (fun x => !x) (I m) = logic2 (fun x x_1 => x != x_1) (I m) (I minusOne)
Tactic:
simp [logic1, logic2, ih]
Proof state after:
no goals
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
m : FinInt sz
⊢ logic1 (fun x => !x) (O m) = logic2 (fun x x_1 => x != x_1) (O m) (I minusOne)
Tactic:
simp [logic1, logic2, ih]
Proof state after:
no goals
Theorem: FinInt.sub_toUint
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n - m) = mod2 (toUint n - toUint m) sz
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.sub_toUint_cong2
Proof state before:
sz : ℕ
m n : FinInt sz
⊢ toUint (n - m) ≡ toUint n - toUint m [2^sz]
Tactic:
simp [cong2, toUint_mod2]
Proof state after:
sz : ℕ
m n : FinInt sz
⊢ toUint (n - m) = mod2 (toUint n - toUint m) sz
Theorem: FinInt.sub_toUint_cong2
Proof state before:
sz : ℕ
m n : FinInt sz
⊢ toUint (n - m) = mod2 (toUint n - toUint m) sz
Tactic:
apply sub_toUint
Proof state after:
no goals
Theorem: FinInt.zext_toUint
Proof state before:
sz₁ sz₂ : ℕ
n : FinInt sz₁
⊢ toUint (zext sz₂ n) = mod2 (toUint n) sz₂
Tactic:
simp [zext, toUint_ofInt]
Proof state after:
no goals
Theorem: FinInt.zext_toUint'
Proof state before:
sz₁ sz₂ : ℕ
n : FinInt sz₁
⊢ sz₁ < sz₂ → toUint (zext sz₂ n) = toUint n
Tactic:
sorry
Proof state after:
no goals
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run ⟦ LHS r₁ r₂ ⟧ (INPUT b) = run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[LHS]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        [])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        [])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_denoteRegion]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
rw[run_seq]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteTypedArgs [] []) (INPUT b) with
    | Except.ok (PUnit.unit, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteTypedArgs [] []) (INPUT b) with
    | Except.ok (PUnit.unit, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_denoteTypedArgs_nil]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteOps scf
        [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteOps scf
        [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp [run_denoteOps_singleton]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteOp scf
        (Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])))
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteOp scf
        (Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])))
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_denoteOp]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        let args ← denoteOpArgs scf [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]
        OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
            (Semantics.semantics_op (IOp.mk "scf.if" [] args (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        let args ← denoteOpArgs scf [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]
        OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
            (Semantics.semantics_op (IOp.mk "scf.if" [] args (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_bind]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteOpArgs scf [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]) (INPUT b) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteOpArgs scf [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]) (INPUT b) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_denoteOpArgs_cons_]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      run
        (do
          let x ← TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")
          let xs ← denoteOpArgs scf []
          pure ({ fst := MLIRType.int Signedness.Signless 1, snd := x } :: xs))
        (INPUT b) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      run
        (do
          let x ← TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")
          let xs ← denoteOpArgs scf []
          pure ({ fst := MLIRType.int Signedness.Signless 1, snd := x } :: xs))
        (INPUT b) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_bind]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")) (INPUT b) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")) (INPUT b) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[INPUT]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b"))
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b"))
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
rw[run_TopM_get_]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "b") (MLIRType.int Signedness.Signless 1)
                (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "b") (MLIRType.int Signedness.Signless 1)
                (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[SSAEnv.get_set_eq]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        run (denoteOpArgs scf [])
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        run (denoteOpArgs scf [])
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[run_denoteOpArgs_nil]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      run (pure [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }])
        (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      run (pure [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }])
        (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[run_pure]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[TopM.mapDenoteRegion]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[OpM.denoteRegions]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[Semantics.semantics_op]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (scf_semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (scf_semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[scf_semantics_op]
Proof state after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (ite (b = false → False) (OpM.denoteRegion r₁ 0) (OpM.denoteRegion r₂ 1) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)