Stream: Miscellaneous

Topic: ✔ Stuck in confluence for inductive types

walker (Jul 07 2023 at 21:58):

mini-mission accomplished: confluence proved!

I learned a lot of lessons including how to circumvent the strict positivity checks in coq:
I defined seq_forall_pair as:

Definition seq_forall_pair A B (R: A -> B -> Prop) s1 s2 :=
    size s1 = size s2 /\ forall ts, PIn ts (zip s1 s2) -> R (ts.1) (ts.2).

And I used this everywhere instead of what I had before, also it was good exercise in writing custom induction principles for reduction and conversion.

once again thanks a lot for all the help and the idea.

Notification Bot (Jul 07 2023 at 22:00):

walker has marked this topic as resolved.

Last updated: Nov 29 2023 at 21:01 UTC