Conditional Resolution Tactics

This file provides tactics for resolving conditional branches in relational proofs, inspired by EasyCrypt's rcondt and rcondf tactics.

Main tactics

• ssprove_rcondt - resolve a conditional when condition is always true
• ssprove_rcondf - resolve a conditional when condition is always false
• ssprove_ite - try to resolve conditionals automatically

Main lemmas

• rHoare_ite_true - if condition is true under precondition, reduce to then-branch
• rHoare_ite_false - if condition is false under precondition, reduce to else-branch
• rHoare_ite_left_true/false - asymmetric: condition on left side only
• rHoare_ite_right_true/false - asymmetric: condition on right side only

Design rationale

Crypto games are full of if b then ... else ... branches. In many proofs, the precondition (invariant) determines which branch is taken. EasyCrypt's rcondt/rcondf tactics automate this pattern. Without these tactics, users must manually simp [h] or split_ifs, which is verbose and fragile.

References

• EasyCrypt: rcondt, rcondf tactics
• CatCrypt: manual branch resolution via simp

Symmetric if-then-else rules (same condition both sides)

theorem CatCrypt.Relational.rHoare_ite_true {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {c : Bool} {t₁ e₁ : Core.SPComp α} {t₂ e₂ : Core.SPComp β} (hc : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → c = true) (ht : rHoare Φ t₁ t₂ Ψ) : rHoare Φ (if c = true then t₁ else e₁) (if c = true then t₂ else e₂) Ψ

If condition is true under the precondition, reduce both sides to then-branch.

theorem CatCrypt.Relational.rHoare_ite_false {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {c : Bool} {t₁ e₁ : Core.SPComp α} {t₂ e₂ : Core.SPComp β} (hc : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → c = false) (he : rHoare Φ e₁ e₂ Ψ) : rHoare Φ (if c = true then t₁ else e₁) (if c = true then t₂ else e₂) Ψ

If condition is false under the precondition, reduce both sides to else-branch.

Asymmetric rules (condition on one side only)

theorem CatCrypt.Relational.rHoare_ite_left_true {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {c : Bool} {t₁ e₁ : Core.SPComp α} {c₂ : Core.SPComp β} (hc : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → c = true) (ht : rHoare Φ t₁ c₂ Ψ) : rHoare Φ (if c = true then t₁ else e₁) c₂ Ψ

Left side has condition true, right side is unconditional.

theorem CatCrypt.Relational.rHoare_ite_left_false {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {c : Bool} {t₁ e₁ : Core.SPComp α} {c₂ : Core.SPComp β} (hc : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → c = false) (he : rHoare Φ e₁ c₂ Ψ) : rHoare Φ (if c = true then t₁ else e₁) c₂ Ψ

Left side has condition false, right side is unconditional.

theorem CatCrypt.Relational.rHoare_ite_right_true {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c : Bool} {t₂ e₂ : Core.SPComp β} (hc : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → c = true) (ht : rHoare Φ c₁ t₂ Ψ) : rHoare Φ c₁ (if c = true then t₂ else e₂) Ψ

Right side has condition true, left side is unconditional.

theorem CatCrypt.Relational.rHoare_ite_right_false {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c : Bool} {t₂ e₂ : Core.SPComp β} (hc : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → c = false) (he : rHoare Φ c₁ e₂ Ψ) : rHoare Φ c₁ (if c = true then t₂ else e₂) Ψ

Right side has condition false, left side is unconditional.

Decidable condition versions

These handle if (decide P) then ... patterns, which are common when conditions are decidable propositions rather than booleans.

theorem CatCrypt.Relational.rHoare_dite_true {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {P : Prop} [inst : Decidable P] {t₁ : P → Core.SPComp α} {e₁ : ¬P → Core.SPComp α} {t₂ : P → Core.SPComp β} {e₂ : ¬P → Core.SPComp β} (hp : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → P) (ht : ∀ (h : P), rHoare Φ (t₁ h) (t₂ h) Ψ) : rHoare Φ (dite P t₁ e₁) (dite P t₂ e₂) Ψ

If a decidable proposition holds under precondition, take then-branch.

theorem CatCrypt.Relational.rHoare_dite_false {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {P : Prop} [inst : Decidable P] {t₁ : P → Core.SPComp α} {e₁ : ¬P → Core.SPComp α} {t₂ : P → Core.SPComp β} {e₂ : ¬P → Core.SPComp β} (hp : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → ¬P) (he : ∀ (h : ¬P), rHoare Φ (e₁ h) (e₂ h) Ψ) : rHoare Φ (dite P t₁ e₁) (dite P t₂ e₂) Ψ

If a decidable proposition fails under precondition, take else-branch.

Code-level if-then-else equality lemmas

These lemmas state that if a condition is known, if-then-else simplifies. Useful for rewriting inside SPComp terms.

theorem CatCrypt.Relational.SPComp.ite_true_eq {α : Type u_1} {c : Bool} {t e : Core.SPComp α} (hc : c = true) : (if c = true then t else e) = t

If condition is true, if c then t else e = t at SPComp level.

theorem CatCrypt.Relational.SPComp.ite_false_eq {α : Type u_1} {c : Bool} {t e : Core.SPComp α} (hc : c = false) : (if c = true then t else e) = e

If condition is false, if c then t else e = e at SPComp level.

Conditional Resolution Tactics

def CatCrypt.Tactics.tacticSsprove_rcondt : Lean.ParserDescr

ssprove_rcondt resolves a conditional branch by proving the condition is true.

When the goal has if c then t else e on one or both sides of an rHoare judgment, and the precondition implies c = true, this tactic simplifies to the then-branch.

Generates a subgoal for proving c = true under the precondition.

Example:

theorem example (hb : ∀ h₁ h₂, Φ h₁ h₂ → b = true) :
    rHoare Φ (if b then t₁ else e₁) (if b then t₂ else e₂) Ψ := by
  ssprove_rcondt
  · exact hb  -- prove condition is true
  · ...       -- prove rHoare Φ t₁ t₂ Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_rcondt = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_rcondt 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_rcondt" false)

def CatCrypt.Tactics.tacticSsprove_rcondf : Lean.ParserDescr

ssprove_rcondf resolves a conditional branch by proving the condition is false.

When the goal has if c then t else e on one or both sides of an rHoare judgment, and the precondition implies c = false, this tactic simplifies to the else-branch.

Generates a subgoal for proving c = false under the precondition.

Example:

theorem example (hb : ∀ h₁ h₂, Φ h₁ h₂ → b = false) :
    rHoare Φ (if b then t₁ else e₁) (if b then t₂ else e₂) Ψ := by
  ssprove_rcondf
  · exact hb  -- prove condition is false
  · ...       -- prove rHoare Φ e₁ e₂ Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_rcondf = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_rcondf 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_rcondf" false)

def CatCrypt.Tactics.tacticSsprove_ite : Lean.ParserDescr

ssprove_ite tries to resolve if-then-else branches automatically.

This tactic first tries split_ifs and then attempts to close goals with simp_all, assumption, or decide.

Example:

theorem example : rHoare Φ (if true then t₁ else e₁) c₂ Ψ := by
  ssprove_ite

Equations

• CatCrypt.Tactics.tacticSsprove_ite = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_ite 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_ite" false)