search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

Bug in forgetting with letin #58

Open tlringer opened 5 years ago

tlringer commented 5 years ago

This fails:

Definition append_vect (A : Type) (pv1 : sigT (vector A)) (pv2 : sigT (vector A)) :=
  let pv := append_vect_inner A pv1 pv2 in
  existT _ (projT1 pv) (projT2 pv).

Lift list vector in append as append_vect_lifted.

While this succeeds:

Definition append_vect (A : Type) (pv1 : sigT (vector A)) (pv2 : sigT (vector A)) :=
  existT _ (projT1 (append_vect_inner A pv1 pv2 )) (projT2 (append_vect_inner A pv1 pv2 )).

Lift list vector in append as append_vect_lifted.

Since we get an intermediate (vector A) in an unexpected place even though it eventually goes away. We should support this somehow. Forgetting in general is not very useful when going along the equivalence we have, honestly; would be better to use the other equivalence for this.