search

vafeiadis / hahn

Hahn: A Coq library
MIT License
29 stars 15 forks source link

Is there a limit of sin_rewrite etc. ? #36

Open JonasOberhauser opened 2 months ago

JonasOberhauser commented 2 months ago 
Goal forall a b c d e f g h i : relation actid, a ⨾ b ⨾ c ⨾ d ⨾ e ⨾ f ⨾ g ⨾ h ⨾ i ⊆ ∅₂.
Proof.
  intros.
  arewrite (a ⨾ b ⨾ c ⨾ d ⨾ e ⨾ f ⨾ g ⨾ h ⊆ ∅₂).

fails. Am I doing something wrong or did I reach some internal limit of sin_rewrite etc?

JonasOberhauser commented 2 months ago

If it's an internal limit, would it be much effort to switch to this: https://github.com/coq-community/aac-tactics ? This could also work for ∩ etc.