Questions tagged [strategy]

When creating proofs there are strategies and tactics. Use this tag when seeking a high level way of doing a proof or part of a proof. If instead you have a high level plan but do not know the rules of inference to use then consider the tactics tag.

Filter by
Sorted by
Tagged with
2 votes
1 answer

How to unfold definitions in Lean / find the right theorems to apply?

After a few days playing around with Lean4, I notice I keep running into the problem of how to find the right theorems to apply. The situation below is one I run into particularly often, so perhaps I ...
5 votes
1 answer

How to implement first-order relational structures in Coq?

I'm trying to define a first-order relational structure in Coq. I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough. I also have a ...
  • 2,593