working on algorithmic subtyping

[HuStmpHrrr]

c.f. #121

[HuStmpHrrr]

Some lemmas are left behind now, including the completeness proof.

but basically what we have now shows indeed algorithmic subtyping is structural in normal forms.

[HuStmpHrrr]

When proving subtyping in the Pi case, I noticed another problem. Now the algorithm first normalizes both sides and then just recurses on normal forms to decide subtyping. It looks right but the completeness proof is blocked.

Consider Pi A B and Pi A' B'. The algorithm normalizes B to some N with an extended environment of A. The problem now, is the declarative subtyping can only confirm a subtyping relation between B and B' when the context is extended with A'. So the inductive argument doesn't go through.

I am not sure how to fix it. I hope it doesn't involve a complicated semantic setup. I somehow feel that the subtyping is just a fancy way of propagating cumulativity so it shouldn't be this difficult. I think the solution might just be to relate the normal forms of B obtained in different contexts, as we know A' is a subtype of A.

[HuStmpHrrr]

I think the solution probably lies in the PER model of contexts, which we will have to express anyways. A lazyman's fix at this moment is to only say A is equivalent to A', but as I pointed out in CoqClub, this induces some issue in the type theory.

[Ailrun]

How about this algorithm?

1. For given G and G' where G is sub-context of G' normalize M in G and M' in G'.
2. decide normal form subtyping for W and W' (the normal forma obtained by the above step)
3. This gives us G |- M sub M'

This algorithm is definitely sound as we have G |- M ~~ W, G |- W sub W' and G' |- W' ~~ M (which can be "lowered" to G |- W' ~~ M and this the conclusion. The question is now more on completeness logrel for this I guess.

[HuStmpHrrr]

How about this algorithm?

1. For given G and G' where G is sub-context of G' normalize M in G and M' in G'.

2. decide normal form subtyping for W and W' (the normal forma obtained by the above step)

3. This gives us `G |- M sub M'`

This algorithm is definitely sound as we have G |- M ~~ W, G |- W sub W' and G' |- W' ~~ M (which can be "lowered" to G |- W' ~~ M and this the conclusion. The question is now more on completeness logrel for this I guess.

this is basically what is doing here. I am giving up on contra-variant subtyping. too many things fail on my end.

[HuStmpHrrr]

should merge #127 first

[Ailrun]

this is basically what is doing here. I am giving up on contra-variant subtyping. too many things fail on my end.

The previous one is using same Gamma, not Gamma and Gamma' under a sub-context relation. But anyway, I'm all good for not having contravariant subtyping.