I was reading a paper where they showed a technique of showing a technique which I thought I might borrow for different purpose:

So The goal is to show a language with set of operational semantics, and typing rules have the same properties of another language

Ideally, I wanted show that progress and preservation can be carried from one language to another.

My goal was to have a an richer MLTT implementation and try to cheat the system and get proofs of progress and preservation by showing that anything done in this language can be done in a simpler MLTT language.

So I started by `Term`

and `CTerm`

which is core language term.

Then I created a simple function to translate terms to core terms:

```
Fixpoint translate (t: Term) : CTerm :=
match t with
| var idx => Cvar idx
| univ lvl => Cuniv lvl
| pi A B => Cpi (translate A) (translate B)
.....
end.
```

They are identical as you can see, bec. my current goal is to identify the fundamental problems.

I was able to prove that this translation preserves structure by making sure that it preserves typing, substitution, and reduction:

```
Lemma translate_preserve_subst_term (t n: Term): translate t.[n/] = (translate t).[translate n/].
Lemma translate_preserve_typing Γ t T:
Γ t ⊢ T -> map translate Γ ⊢ (translate t) : (translate T).
Lemma translate_preserve_mred t1 t2:
t1 ⟶* t2 -> (translate t1) ⟶* (translate t2).
```

Note I am abusion the notation abit but my problem is not a problem of coq anyway it is problem with the technique.

So now that I have proofs of preserving structure, I want to prove, confluence.

I know that:

```
Lemma core_mred_confluence (t1 t2 t: CTerm)
t ⟶* t1 ->
t ⟶* t2 ->
exists t',
t1 ⟶* t' /\ t2 ⟶* t'.
```

and I wanted to prove that:

```
Lemma mred_confluence (t1 t2 t: Term)
t ⟶* t1 ->
t ⟶* t2 ->
exists t',
t1 ⟶* t' /\ t2 ⟶* t'.
```

using `translate_preserve_mred`

and the `core_mred_confluence`

lemma I was stuck at proving:

```
t3: CTerm
=================
CMulti CReduction (translate t1) t3 ->
CMulti CReduction (translate t2) t3 -> exists t' : Term, t1 ⟶* t' /\ t2 ⟶* t'
```

and it feels like I need to get the inverse translation, that would work for this particular case, because both languages are identical, but I would intend to add multi-argument functions/pairs/ and moules, then translation would lose information since the core language has only the basic tuples, and single argument functions. Also I indented to remove annotations required for bidirectional type checking like:

`lam A t`

=> `core_lam t`

but then inverting this operations using only the expression is impossible.

So my question is: is this technique known ?(the goal is to avoid having to deal with the full proofs of progress and preservation everytime I make a modification to the language I am building)

B- if yes, I don't even know what is it called and I cannot search for it in literature, and I don't know where did I go wrong with my proof strategy.

C- If now, what would be the right way to go with my goal of diving the language design into core theory and elaboration and prove that the elaboration maintains all the (arbitrary) properties of the core.

sounds like https://hal.inria.fr/hal-01445835/

btw for reduction you might not have the other direction ie `forall t1 t2, (translate t1) ⟶* (translate t2) -> t1 ⟶* t2`

but still have something close like `forall t1 ct2, (translate t1) ⟶* ct2 -> exists t2, ct2 ⟶* (translate t2) /\ t1 ⟶* t2`

I thought this paper was just a survery, but I see lots of interesting ideas! thanks alot for reminding me of it!

wow first time I checked it, it didn't make sense, and now everything sounds familiar!

Gaëtan Gilbert said:

btw for reduction you might not have the other direction ie

`forall t1 t2, (translate t1) ⟶* (translate t2) -> t1 ⟶* t2`

but still have something close like`forall t1 ct2, (translate t1) ⟶* ct2 -> exists t2, ct2 ⟶* (translate t2) /\ t1 ⟶* t2`

right that should work and I hope it does, I was so fixated on the idea that inverse translation is to be avoided thanks for the hint

@Gaëtan Gilbert I tried following that lead you gave me,

The problem is is using the lemma "forall t1 ct2, (translate t1) ⟶* ct2 -> exists t2, ct2 ⟶* (translate t2) /\ t1 ⟶* t2` is that it doesn't tell much about ct2, I couldn't use it to lift confluence from core language to elaborate language:

We start from here:

```
t ⟶* t1 ->
t ⟶* t2 ->
exists t', t1 ⟶* t' /\ t2 ⟶* t'.
```

then we translate to core terms:

```
(translate t) ⟶* (translate t1) ->
(translate t) ⟶* (translate t2) ->
exists t', t1 ⟶* t' /\ t2 ⟶* t'.
```

Then we use confluence the core language:

```
(translate t1) ⟶* ct' ->
(translate t2) ⟶* ct' ->
exists t' : Term, t1 ⟶* t/\ t2 ⟶* t
```

using the inverse lemma: one gets something like:

```
(exists A' : Term, translate A' :=ct' /\ t2 ⟶* A') ->
(exists A' : Term, translate A' := ct' /\ t1 ⟶* A') ->
exists t'0 : Term, t1 ⟶* t'0 /\ t2 ⟶* t'0
```

Which doesn't look far of the starting point.

The confluence property is lost once you go back, and I feel stuck.

This partial inverse of translation is too weak, the proper inverse is too strong, and I feel totally stuck.

I also created a translation judgement in the hope it might be make things easier to work with:

```
Reserved Notation "'⟦' x '⟧' ':=' y" (at level 20, y at next level).
Inductive Translate: Term -> CTerm -> Prop :=
| Translate_var idx : ⟦ var idx ⟧ := Cvar idx
| Translate_univ lvl : ⟦univ lvl⟧ := Cuniv lvl
| Translate_pi A B A' B':
⟦A⟧ := A' ->
⟦B⟧ := B' ->
⟦pi A B⟧ := Cpi A' B'
| Translate_lam A t A' t' :
⟦A⟧ := A' ->
⟦t⟧ := t' ->
⟦lam A t⟧ := Clam A' t'
| Translate_appl m n m' n':
⟦m⟧ := m' ->
⟦n⟧ := n' ->
⟦appl m n⟧ := Cappl m' n'
| Translate_sigma A B A' B':
⟦A⟧ := A' ->
⟦B⟧ := B' ->
⟦sigma A B⟧ := Csigma A' B'
| Translate_pair A B m n A' B' m' n':
⟦A⟧ := A' ->
⟦B⟧ := B' ->
⟦m⟧ := m' ->
⟦n⟧ := n' ->
⟦pair A B m n⟧ := Cpair A' B' m' n'
| Translate_proj1 m m':
⟦m⟧ := m' ->
⟦proj1 m⟧ := Cproj1 m'
| Translate_proj2 m m':
⟦m⟧ := m' ->
⟦proj2 m⟧ := Cproj2 m'
where "'⟦' x '⟧' ':=' y" := (Translate x y) (format "⟦ x ⟧ := y").
```

what I want to avoid doing is assuming that translation has inverse, because I plan to lose some information in future iterations from the core language ( like A B parts in sigma which is used for type annotations)

That makes it feel like the type system is not actually confluent, because then in this particular case (which I still doesn't have)

`⟦pair (univ 1) (univ 2) m n⟧ := Cpair m' n'`

and `⟦pair (var 1) (var 2) m n⟧ := := Cpair m' n`

, but then the two translations reduce to one another by reflexivity, but the two original terms does not for obvious reasons.

which makes me wonder if the general assumption "if lang X can be embedeed in lang Y, and lang Y has properties A, B, C, then lang X also has the properties A, B, C" is actually wrong ?

I think I found name of the property I need, "Conservativity"

which makes me wonder if the general assumption "if lang X can be embedeed in lang Y, and lang Y has properties A, B, C, then lang X also has the properties A, B, C" is actually wrong ?

If you lose information, can it be called an embedding?

But my assumption is if a language is

Type safe, then that language with extra annotations should also be type safe

Especially if this annotations does not restrict the language usage, and does not allow extra theorems to be proven.

A message was moved here from #Miscellaneous > Content about System F (Polymorphic Lambda Calculus)) by walker.

It might be easier to construct counter-examples: take erasure from simply-typed lambda calculus to un(i)typed lambda calculus, and patch STLC to fail preservation

In general, weakening typing doesn't necessarily weaken preservation: Typing appears both co- and contravariantly in the statement, after all

but then why would everyone say that if there is structure preserving transformation from A to B, then proving that B is safe is sufficient to prove that A is safe (or a variant of that) ?

let me check the paper

"To justify a complex type theory, it suffices to compile it into a simpler—already justified—type theory.”

in the The next 700 syntactical models of type theory paper.

but they never proved this statement which is confusing.

because "justify" is a variety of properties

same way you didn't define what "safe" means

I see, that is unfortunate, I though it would be possible to move proofs of progress& preservation to richer type theory.

However, do you really need to consider reduction on the source language, instead of only the target language?

There isn't a notion of reduction on Coq source terms, only on the Coq terms produced by elaboration

What I am currenty doing is trying to use the source language as the main language,I wanted to enahnce it with enough structure that will be important when doing code generation to assembly/SSA-like IR,

so what is really needed here is to have evidence that this source language has 2 properties, type safety, desirable type checking (assuming normalization)

To prove the bidirectional type checker, I often used the confluence property in the proofs, so I need that. As for the type safety, i need to show the source language has progress&subject reduction.

In principle I can do that from scratch, but I wanted to offload that task to the core language and infer those properties in the source language.

For instance, when adding module system to the source language.

apparently this property I need is to some extent studied under the names `conservative extension`

,`definitional extension`

, `conservative transformations`

and they have not been formalized in any proof system before.

the question is : is proving one of those three properties easier than proving type safety by other means ? and I could't find definite answer for that.

Last updated: Dec 01 2023 at 07:01 UTC