Generally I have three properties:

A B C

In principle I cannot prove that A x y-> C x y by induction on A.

But If I can restrict my self to `x`

and `y`

that is also `B x`

& `B y`

then It feels like I can prove it.

The obvious solution would be to construct A such that `forall x y, A x y -> Bx /\ By`

but that will be extremely complicated and I want to avoid it:

The second obvious solution would be to prove `A x y-> B x -> By ->C x y`

but that does not work, because one of the cases of A is basically a transitivity:

```
Induvite A ......
| A_trans: A x y -> A y z -> A x z
```

So here we get a third `y`

without the repsective `B y`

Also `forall x, B x`

does not hold, and assuming that will be too strong, so I cannot do: ` (forall x, B x) -> A x y -> C x y`

The question here is .. is there a way to do something that allows me to do induction over A but maintain the invariant that any variable I get,I also get the proof `B x`

with it ?

I want to avoid modifying `A`

at all cost, because 5k locs depend on it.

Edit:

What I want is to do induction on something like

` A x y /\ B x /\ By`

Such that every element I get I also get the `B`

property of it

I may be overlooking something, but I think your question as it stands is not straightforward at all.

`A`

including transitivity immediately makes this much harder. Essentially, you need to be able to show that if you have a proof of `A x y`

, then it was obtained without ever using transitivity over a variable `z`

for which `B`

does not hold. So another way to look at the problem is to write a second definition of `A`

with restricted transitivity, say `A'`

, and show that if `B x`

and `B y`

then `A x y <-> A' x y`

or something like that. You then prove your property about `A'`

by induction and about `A`

through the equivalency with `A'`

.

Note that I'm basically describing cut elimination here. Some systems have it and some don't, and when they have it, it's not necessarily trivial to prove.

You don't quite need full cut elimination though, simply a way to restrict transitivity to well-behaved formulas, something like:

```
A_Btrans : B y -> A x y -> A y z -> A x z
```

instead of your unrestricted `A_trans`

.

Alternatively, you may be able to prove a lemma of the form `A x y -> A y z -> exists y', B y' /\ A x y' /\ A y' z`

, which could be useful in your original theorem.

I second Ana: in general, what you want to prove simply cannot be obtained by a simple induction. Given your previous questions, I would guess that `A`

is some kind of (untyped) conversion, and `B`

is a precondition like typing or well-scoping. In general, showing that you can restrict to going only through well-typed/well-formed terms for conversion is a highly non-trivial property! If this is what you are after, I would recommend reading Pure Type System Conversion is Always Typable, which shows more or less this… But takes a whole paper to do so

If the context is Martin-Löf type theory, one can also replace untyped conversion with typed equality. But I understand it's not a small patch, but rather a significant difference between e.g. Coq and Agda, and their metatheories

Yes, absolutely. The equivalence is already hard for PTS, and afaik it's open for any more complicated system…

(Open in the sense that people believe it holds but nobody want to bite the bullet and show it)

well, It is really impressive that you guys were able to identify what the `A`

from that description, so the problem is I was trying to expand `MLTT with untyped conversion`

to `MLTT with untyped conversion and basic module system`

for the time being it is just one module (it is literally a name space), This name space is essential for conversion, so we have the new conversion judgement:

```
"Σ '⊢' t1 '≅' t2" := (Conv Σ t1 t2)
```

This sigma thing is only used for global variables:

```
| Conv_gvar: forall Σ n t,
mod_get_term Σ n = Some t ->
Σ ⊢ gvar n ≅ t
```

Progress and preservations was prooved for this language, but I wanted to prove 1 last thing:

for obvious reasons arbitrary terms cannot be translated to core MLTT because there is no guarantee that arbitrary `gvar "foo123"`

will

exist in sigma.

That required a notion of well formed term that guarantee the previous property, that gave rise to well formed terms, well formed gammas, and well formed sigma (the last two are weaker than well formed contexts required by typing rules) , and the translation function looked as follows:

```
"'⟦' Σ ',' t ',' wft ',' wfΣ '⟧'"
```

Otherwise it would have been partial translation

The problem is typing implies well formness of types, and gamma and sigma

But conversion did not

And eventually I need to prove that:

```
Lemma translate_preserve_conv Σ t1 t2 wft1 wft2 wfΣ:
Σ ⊢ t1 ≅ t2 -> (* in the language of MLTT with name space*)
⟦Σ, t1, wft1, wfΣ⟧ ≅ ⟦Σ, t2, wft2, wfΣ⟧. (* MLTT *)
Proof.
```

And here is where transitivity causes problems.

I really want to avoid to make conversion more complex for the sake of this translation proof,

Ah, this is hard because conversion can step through non-well-formed terms, indeed

`1`

and `(𝜆 x. 1) any_term_whatsoever`

are convertible (with untyped conversion)... Meven is saying that such terms can be avoided, but this is hard to prove (EDIT: AFAICT)

what is not clear, is whether this is logical inconsistency or just issue of weak proof by induction.

just induction AFAICT

or rather, you can use induction, but you must first _patch_ the derivation

a proof that `0 + 1 = (𝜆 x. 1) ill_formed_term = 1`

is a problem, but you can produce a different conversion proof that `0 + 1 = 1`

without stepping through `ill_formed_term`

I assume by patching the deriviation you mean make :

`Σ ⊢ t1 ≅ t2 -> TermWF t1`

right ?

I don't necessarily mean modifying how `_ ⊢ _ ≅ _`

is defined; by patching a derivation I meant taking an `x : Σ ⊢ t1 ≅ t2`

(`x`

is the derivation) and producing `y : Σ ⊢ t1 ≅ t2`

such that all intermediate steps are well-formed (and we get a proof of that fact).

typed conversion would avoid these problems and is generally easier for metatheory, but it can be slower to implement directly (https://proofassistants.stackexchange.com/q/720/393 has some discussion)

mmmm, that sounds like extremely complex task, I am not even sure how to start, at least that means I need a judgement for well formed step in conversion or something similar ?

Maybe you can restructure your A so it's defined as `e₁ ≃ e₂ = (e₁ ↝* e₃ ∧ e₂ ↝* e₃)`

. It's usually fairly easy to show that `↝*`

preserves well-formedness.

isn't that the church rosser theorem ?

```
Lemma mred_cr Σ A A':
Σ ⊢ A ≅ A' ->
exists B, Σ ⊢ A ⟶* B /\ Σ ⊢ A' ⟶* B.
```

I think I already have that

actually I have the iff version of it as well, right that is briliant idea, thanks @Stefan Monnier

Should the untyped-typed equivalence follow? Guess not since it's an harder theorem, but why?

OTOH the paper Meven cited might be harder because it works on arbitrary PTS, rather than a disciplined class or a specific example

Paolo Giarrusso said:

typed conversion would avoid these problems and is generally easier for metatheory

It depends: untyped conversion means you have to treat the possibility of nasty untyped terms in your conversion. But on the other hand, it has the nice advantage that you can prove properties of conversion independently of typing, since they are not mutually defined. In some cases, this makes your life much easier. For instance, things like "typed confluence" are quite annoying, because you need to handle the types, which means you want to prove properties of them, but some of these are consequences of confluence itself… This is the main issue they are facing in showing the equivalence between PTS with typed and untyped conversion (and their solution is to introduce a third system to be able to cut the knot)

walker said:

isn't that the church rosser theorem ?

Yes, showing equivalence between "freely defined" conversion (ie, with a transitivity rule) and the one defined as "reduction to equal terms" is morally a form of confluence/Church-Rosser

Paolo Giarrusso said:

Should the untyped-typed equivalence follow? Guess not since it's an harder theorem, but why?

Yes, it does follow, but the problem is to do a proof of *typed* confluence, which is tricky (much more than the untyped version of it)

Being in a general PTS (especially, non-functional) makes things harder, but I don't think this is so crucial, already for a "nice" PTS the problem is non-trivial

As for the original question: this is indeed a defect of conversion containing "too many" useless (in the sense that they don't let you derive more interesting things) but annoying (in the sense that they screw up your proof by induction) derivations. And the way to patch it is to somehow get rid of these useless-but-annoying derivations.

The standard way, as Stefan suggests, is to show equivalence of conversion with another relation (typically, reduction to a common term) that does not have annoying derivations. So you'd first show that if two terms are convertible, then they reduce to a common term (Church-Rosser), then translate only those proofs on conversion, and hopefully these more specific kinds of derivation you *can* translate, because well-formation is preserved by reduction (this might even be easier to show than preservation of typing).

Last updated: Oct 04 2023 at 23:01 UTC