PL|PL 2020-2 QE Proof PL2020-2QEProof

original question

文章图片

文章图片

文章图片
Claim :
【PL|PL 2020-2 QE Proof】Proof by induct on :

:
the goal become,In this case by inversion precedence in goal with respect to rule Prefix we can know,can only be 0 and at this time claim holds
:
by rewriting the second definition of sort, then the goal become:
.
by rule Prefix we can know,can only beand we can always find exists . And union something is always larger than itself so claim holds
Similar operation to before, the goal become:
.
by rule Choice1 and Choice2 we can see, we can always find ato let precedence hold, andcan become eitheror. union of set is monotonic, of course larger. Clearly claim holds.
The goal become:

similar inversion, this time we have 3 interesting case
- by rule Par1 : we can have, which means by 4th rule of sort we can have. By inductive hypothesis we can know ifis the derivation ofthen we will haveso clearly final goal is true
- Par2 and Par3 are similar. the only difference in Par3 is bothandcause a shrink the size of set.
The goal become:

By rule Restrict we can knowcan become , according to the last rule of sort we can rewritein the goal as. And according to inductive hypothesis, we can know . So clearly claim hold.