search

sr-lab / coqpyt

Python client for coq-lsp
MIT License
25 stars 3 forks source link

tactics and theorems with the same name #24

Open Nfsaavedra opened 11 months ago

Nfsaavedra commented 11 months ago 
Class Reflexive (R : A -> A -> Prop) := reflexivity : forall x : A, R x x.

The statement above from the Coq standard library generates a theorem called reflexivity. This theorem can be used with apply reflexivity, but the tactic reflexivity can still be used as well. This is a problem since when we are collecting our context the statement above will be linked to the tactic reflexivity, even when it shouldn't.

Our context should allow equal names with different term types and then somehow figure out what is the correct term type to be collected in different situations.

Nfsaavedra commented 11 months ago

There is also a problem captured in a non-deterministic way in our tests where instead of the statement in the previous comment we get:

Class Reflexive (R : crelation A) := reflexivity : forall x : A, R x x.