theowinterhalter / formal-type-theory Goto Github PK

And then remove myptt.v. This needs to be done carefully as some proof might break.

Currently there's both formalization/inversion.v and formalization/ptt_inversion.v. We could have just one of them, preferably configuration-agnostic.

SubstZero

       Γ ⊢ u : A
------------------
{u}(Γ,A) : Γ → Γ,A

When we want to apply the induction hypothesis for the translation we need to provide a translation for A that we don't have.
One fix would be to add Γ ⊢ A type as a premise.

I checked rapidly against the whole type system and it appears to me that only WeakZero and maybe EqSubstZeroSucc might have a similar problem.
In that case adding the premises wouldn't be a big deal.

I know we decided at some point to remove context annotations on substitutions, but I'm still not sure this was a good idea. On the contrary I'd advocate for full annotation: nothing should be guessed.

Otherwise, I fear that cases like SubstShift will not be solvable as soon as we use inversion (as it will introduce a new context every time).

In the translation we have the notion of equivalence between types and between terms.
They need a definition.

For type equivalence we could probably use type coercions (possibly over the identity context coercion).
However, for terms, it is unclear.

We also discussed typing for CTT.

Presently (in branch translation), CTT comes with term' and term where

term : Type :=
     | coerce : termCoerce -> term' -> term

So it is possible to come up with

isterm' : context -> term' -> type -> Type

and

isterm : context -> term -> type -> Type

where the latter deals with coercions.

However the question becomes harder for equality judgements, and raises the question of whether we should have coercion judgements.

@andrejbauer suggested we instead defined ITT and an evaluation function from CTT to ITT and only rely on typing for the evaluated terms in the translation.

Prove it in PTT and deduce it holds for ETT?

We could probably repurpose preadmissibility.v for it and then remove sanity.v altogether.

σ : Γ → Δ          Δ ⊢ A type
------------------------------
   (σ|Γ,A) : Γ,A[σ] → Δ,A

When translating this rule, we first assume we are given a translation of Γ,A[σ].
By homology, we get that this is some Γ',A'[σ']. By inversion of typing, we get that σ' : Γ' → Δ' for some Δ'. The thing is, we have no way to know that this Δ' is a translation of Δ.

For now it is not a requirement the way we stated the theorem, but this is probably something we want for composition of substitutions for instance.

σ : Γ → Δ             θ : Δ → Ξ
-------------------------------
         σ ∘ θ : Γ → Ξ

@andrejbauer has the layout on his computer of a theorem we would like to prove about eliminating substitutions.

I added composition of substitutions and it doesn't carry any context information.
I don't know if it should for similar reasons as for the application.

I wonder if you could come up with a theorem that says that we are safe for this aspect.
What do you think?

The stuff involving J is indigestible. Either we need to come up with sugar that makes it pallatable, or we find out a better way of doing it. I'd prefer not to extend substitutions even further to accommodate J, but there may not be a better way.

The PDF file rule.pdf advertised that it contains all the rules as if all the flags were on. However, as far as I can tell it actually doesn't display any of the rules that require a condition flag. For example, in tt.v there is a rule TyProd which follows TySubst and depends on the flag withpi, but this rule does not appear in the PDF.

Let's take the example of context coercions.

Structure contextCoercion :=
  { ctxco_map : itt.substitution
  ; ctxco_inv : itt.substitution
  }.

Definition isContextCoercion c G D := (
  itt.issubst (ctxco_map c) G D *
  itt.issubst (ctxco_inv c) D G *
  (forall A u,
     itt.isterm D u A ->
     { p : itt.term
     & itt.isterm D p (itt.Id A (itt.subst (itt.subst u (ctxco_map c)) (ctxco_inv c)) u)
     }
  ))%type.

Presently it seems—correct me if I'm wrong—they are not invertible (the inverse operation being the swap of the two substitutions).
We probably need to add another identity, but I'm unsure about that when thinking about the n-Types of HoTT.

When this is decided, we should address the well-typedness of coercion composition as well.
Same goes for the identity.

We could use Travis to make sure that everything compiles at every commit/push and to run scripts similar to verify.sh if we keep it around.

I just ran

all: keep_eq

having 5000 subgoals and it is already taking quite some time.

As a reminder, this is what keep_eq does:

Ltac keep_eq :=
  doConfig ;
  lazymatch goal with
  | |- eqterm _ _ _ _ => idtac
  | |- eqtype _ _ _ => idtac
  | |- eqsubst _ _ _ _ => idtac
  | |- eqctx _ _ => idtac
  | _ => shelve
  end.

The point is that the magic tactic is bound to take some time if this is already that long.
The faulty one is most probably doConfig as it tries to normalise everything in the context and goal.

Any hope of fixing that?

ITT is used as the ultimate target of the translation.
For it we need it to be sane.
Problem: For simplicity, I removed type annotation from application, was it wrong?

I don't understand much the python script so I'm putting it here.
The script coq2latex.py needs to be updated with the new formulation of type theory.

Right now I get the error message:

SyntaxError: macro isterm expects 3 arguments but got 10

Only the contexts rules get produced and it stops at the first occurrence of isterm.