Documentation

CatCryptCore.Tactics.FieldClear

field_clear tactic #

Extends field_simp for proofs where the goal denominators are ring-equivalent to provided hypotheses but not syntactically identical (e.g. after (n/D)² expansion or commutative reordering).

Pattern #

field_simp does syntactic matching: a hypothesis h : a ≠ 0 only clears a⁻¹ from the goal if a appears literally as written. After intermediate ring_nf or expansion, the goal denominator may be in a ring-equivalent but syntactically different form (e.g. 1 + 2D + D² vs (1+D)², or Y*X vs X*Y), so the match fails.

Strategy #

Given hypotheses hA : a ≠ 0, hB : b ≠ 0, ..., field_clear auto-derives common variants:

then calls field_simp with the augmented set. Designed for use after the SymPy-witness + set atoms approach (see ~/.claude/skills/rocq-to-lean-porting/field_fsatz_porting.md).

Caveats #

This is a heuristic — it doesn't solve the general problem of ring-equivalent matching. It auto-derives specific variants that arise in Field.fsatz-style algebraic-curve proofs. If a denominator in the goal is in some other ring-equivalent form (e.g. 1 + 2*D*X*Y vs 1 + 2*Y*X*D), the user must either reformulate the hypothesis to match, or extend this tactic.

source
def CatCrypt.Tactic.FieldClear.fieldClear :
Lean.ParserDescr

field_clear [h₁, h₂, ...] augments field_simp's hypothesis list with squared and pairwise-product variants of the supplied nonzero hypotheses, then invokes field_simp plus ring_nf for cleanup.

Usage:

have hA : a ≠ 0 := …
have hB : b ≠ 0 := …
field_clear [hA, hB]
-- behaves like:
--   have hA_sq : a^2 ≠ 0 := pow_ne_zero 2 hA
--   have hB_sq : b^2 ≠ 0 := pow_ne_zero 2 hB
--   have hAB   : a * b ≠ 0 := mul_ne_zero hA hB
--   field_simp [hA, hB, hA_sq, hB_sq, hAB]
--   ring_nf

For specific ring-equivalent forms not caught by this default augmentation, the user can provide them explicitly in the hypothesis list.

Equations
  • One or more equations did not get rendered due to their size.
Instances For