0

can you use the Nat solver in agda-stdlib for proof by contradiction? In particular I have a gnarly bit of algebra I'd rather not do by hand, but I'm not sure how to use a solver to make my life easier. For reference this is the result I want to prove:

{n m : ℕ} → 3 + (n + (3 + (n + (3 + (n + n * (3 + n)))))) ≡ 1 + m + (1 + m + (1 + m + 0)) + 2 → ⊥
Ace shinigami
  • 1,374
  • 2
  • 12
  • 25
  • 1
    You can use the solver to simplify each of the sides, but I don't think it's set up to prove anything other than equations. If ℕ is the free commutative semiring on one generator (which I believe it is, but I can't remember), then it should in principle be possible to augment the existing solver to prove inequalities between polynomials. Also, “proof of a negation” or “refutation” is more correct than “proof by contradiction” in this case. – mudri Oct 14 '22 at 09:32
  • 2
    Actually, come to think of it, your statement is not an inequality of polynomials – it's the non-existence of a solution to a Diophantine equation. That's a lot harder to solve. But maybe you meant `({n m : ℕ} → ...) → ⊥`. – mudri Oct 14 '22 at 09:34

0 Answers0