search

MartyO256 / mechanizing-standard-ml

Mechanizing the metatheory of Standard ML in Beluga using Harpoon
0 stars 0 forks source link

Totality checking for type constructor inversion lemmas #4

Open MartyO256 opened 4 years ago

MartyO256 commented 4 years ago

The output of type-inversion is non-inflationary, as specified in the original mechanization using this reduction declaration:

%reduces D' <= D (type-inversion D _ _ D').

Solving the following theorems using type-inversion in Beluga would require complete induction. See https://github.com/Beluga-lang/Beluga/issues/227.

https://github.com/MartyO256/mechanizing-standard-ml/blob/07d71cd2cbed485449235ad22075701c475b96dc/src/safety/regularity.thm#L2352-L2754

MartyO256 commented 4 years ago

Proving can-map for the recursive type constructor requires complete induction too. https://github.com/MartyO256/mechanizing-standard-ml/blob/714697d4c135f57241a9884d03821baefb02eb2e/src/safety/consistency.thm#L322-L342