search

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
MIT License
51 stars 2 forks source link

Inductive hypotheses in _rect eliminators aren't recognized as inductive hypotheses #16

Open tlringer opened 5 years ago

tlringer commented 5 years ago

This is because of #9 not being done yet. Since they are in Type, they are not recognized. So for example, the tool tries checking this:

checking if f: (λ (n : nat) . (eq nat (Coq.Init.Nat.add (n [Rel 1]) O) (n [Rel 1])))
has type p: (Π (n : nat) . Type Coq.Init.Datatypes.12)

And determines that it doesn't. In contrast:

checking if f: (λ (n : nat) . (eq nat (Coq.Init.Nat.add (n [Rel 1]) O) (n [Rel 1])))
has type p: (Π (n : nat) . Prop)

It determines that it does. But you can use the former inside of nat_rect.

Long-term we want to use good evar hygiene. Short term there might be a workaround.

tlringer commented 5 years ago

Indeed, the anomaly raised is:

Universe Coq.Init.Datatypes.12 undefined.
tlringer commented 5 years ago

Blocked by #9