walker (Feb 15 2023 at 17:20): walker (Feb 15 2023 at 17:20):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
Ana de Almeida Borges (Feb 15 2023 at 17:57):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.
Ana de Almeida Borges (Feb 15 2023 at 18:03):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.
Meven Lennon-Bertrand (Feb 16 2023 at 11:25):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
Paolo Giarrusso (Feb 16 2023 at 11:33):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
Meven Lennon-Bertrand (Feb 16 2023 at 11:47):Yes, absolutely. The equivalence is already hard for PTS, and afaik it's open for any more complicated system…
Meven Lennon-Bertrand (Feb 16 2023 at 11:48):(Open in the sense that people believe it holds but nobody want to bite the bullet and show it)
walker (Feb 18 2023 at 08:29):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,
Paolo Giarrusso (Feb 18 2023 at 08:35):Ah, this is hard because conversion can step through non-well-formed terms, indeed
Paolo Giarrusso (Feb 18 2023 at 08:38):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)
walker (Feb 18 2023 at 08:46):what is not clear, is whether this is logical inconsistency or just issue of weak proof by induction.
Paolo Giarrusso (Feb 18 2023 at 08:49):just induction AFAICT
Paolo Giarrusso (Feb 18 2023 at 08:51):or rather, you can use induction, but you must first _patch_ the derivation
Paolo Giarrusso (Feb 18 2023 at 08:52):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
walker (Feb 18 2023 at 08:56):I assume by patching the deriviation you mean make :
Σ ⊢ t1 ≅ t2 -> TermWF t1 right ?
Paolo Giarrusso (Feb 18 2023 at 09:09):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).
Paolo Giarrusso (Feb 18 2023 at 09:11):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)
walker (Feb 18 2023 at 09:22):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 ?
Stefan Monnier (Feb 18 2023 at 15:59):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.
walker (Feb 18 2023 at 16:41):isn't that the church rosser theorem ?
walker (Feb 18 2023 at 16:42):Lemma mred_cr Σ A A':
Σ ⊢ A ≅ A' ->
exists B, Σ ⊢ A ⟶* B /\ Σ ⊢ A' ⟶* B.
I think I already have that
walker (Feb 18 2023 at 16:42):actually I have the iff version of it as well, right that is briliant idea, thanks @Stefan Monnier
Paolo Giarrusso (Feb 18 2023 at 16:54):Should the untyped-typed equivalence follow? Guess not since it's an harder theorem, but why?
Paolo Giarrusso (Feb 18 2023 at 16:57):OTOH the paper Meven cited might be harder because it works on arbitrary PTS, rather than a disciplined class or a specific example
Meven Lennon-Bertrand (Feb 20 2023 at 10:54):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)
Meven Lennon-Bertrand (Feb 20 2023 at 10:56):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
Meven Lennon-Bertrand (Feb 20 2023 at 10:57):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)
Meven Lennon-Bertrand (Feb 20 2023 at 10:58):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
Meven Lennon-Bertrand (Feb 20 2023 at 11:04):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 13 2024 at 01:02 UTC