Stream: Coq users

Topic: case analysis on ex fails

walker (Mar 12 2024 at 11:54):

I was trying to prove that a function exist by constructing it .... midway somewhere I had a situation similar to this one:

Inductive Term : Set :=
| A  (*and the whole ast*).
Goal (exists B : Term, B = B) -> Term.
Proof.
move => [].  (* Case analysis on sort Set is not allowed for inductive
definition ex.*)

Curiously enough when I change to Inductive Term : Type, It works, so what is really going here? and is there a way to fix it while staying in set?

Gaëtan Gilbert (Mar 12 2024 at 11:55):

I don't understand, your example already has Inductive Term : Set
what is the code that works?

walker (Mar 12 2024 at 11:56):

copy paste error, corrected!

Gaëtan Gilbert (Mar 12 2024 at 11:57):

Inductive ... : Type can implicitly become : Prop when that would not restrict the inductive's elimination

walker (Mar 12 2024 at 11:58):

hmmm ... would that affect the fact that this is real AST that I want to later extract ? ... if it becomes implicitly Prop in one part of the proof, will it be also Prop everywhere else ? or is it local ?

Gaëtan Gilbert (Mar 12 2024 at 11:59):

Inductive Term : Type :=
| A.

Check Term : Prop.

Gaëtan Gilbert (Mar 12 2024 at 12:00):

I guess your real AST will have multiple constructors so Type won't be turned into Prop

walker (Mar 12 2024 at 12:00):

I am still unsure implications of that, :sweat_smile: so It will still be possible to extract Term right?

Gaëtan Gilbert (Mar 12 2024 at 12:01):

if Term is non trivial it won't be turned to Prop
if it is trivial there's no point extracting it but you can add : Set instead of : Type to force it if you want

walker (Mar 12 2024 at 12:07):

hmmm, I tried doing it in type on the real thing, and it still does not work:

Inductive Term : Type :=
| var (idx: nat): Term
| univ (l: nat): Term.

Goal (exists B : Term, B = B) -> Term.
Proof.
move => [].  (* Case analysis on sort Set is not allowed for inductive definition ex.*)

All I need is extract the first projection and return it as it is.

Claude Stolze (Mar 12 2024 at 12:10):

Goal {B : Term | B = B} -> Term.

walker (Mar 12 2024 at 12:12):

changing that will not be easy, is there no other way ?

Gaëtan Gilbert (Mar 12 2024 at 12:17):

basically the whole point of using exists is that there is no other way

walker (Mar 12 2024 at 12:18):

I was under the impression that exists is constructive ? so there is always a witness that can be seen and used

Gaëtan Gilbert (Mar 12 2024 at 12:18):

imagine how foo : (exists B : Term, B = B) -> Term gets extracted, the exists is in Prop so it's erased and you have to come up with a term with no information

Gaëtan Gilbert (Mar 12 2024 at 12:18):

walker said:

I was under the impression that exists is constructive ? so there is always a witness that can be seen and used

That's a meta theorem

walker (Mar 12 2024 at 12:24):

this is super tricky situation! I am worried using {_ : _| _} instead of exists will require rewriting the whole code base.

Gaëtan Gilbert (Mar 12 2024 at 12:28):

worry is useless when you have no choice

walker (Mar 12 2024 at 12:42):

Gaëtan Gilbert said:

worry is useless when you have no choice

oh yes it is was easy check that the whole 40klocs will break, the other choice I have it to take a step back and and think about what I really want.

walker (Mar 12 2024 at 12:45):

the lemma I really want is:

    Σ ⊢ t ≅ t' ->
    Σ ⊢ σ ≅ₛ τ ->
    Σ ⊢ t .[σ] ≅ t'.[τ].

where Σ ⊢ σ ≅ₛ τ is the same as forall (x: nat) Σ ⊢ σ x ≅ τ x `

The challenge is stability under substitution for is not provable for conversion, at least as I tried, bu it is provable for parallel reduction.

I thought I might try to lift th proof from parallel reduction to conversion using church rossser or something

walker (Mar 12 2024 at 12:47):

then I had to to figure this part Σ ⊢ σ ≅ₛ τ :

The lemma I was needed about this property is:

     Σ ⊢ σ ≅ₛ τ <->
    (exists β, Σ ⊢ σ ⟶*ₛ β /\ Σ ⊢ τ ⟶*ₛ β).

Backward part is easily proven, forward part, I need to fill in β .... which is the function I tried to build

walker (Mar 12 2024 at 12:48):

to fill in beta, I needed to use confluence property itself, but this time I needed in not in proof but in function

walker (Mar 12 2024 at 12:52):

the other approach which I didn't explore deeply is to just try to do

    Σ ⊢ t ≅ t' ->
    Σ ⊢ σ ≅ₛ τ ->
    Σ ⊢ t .[σ] ≅ t'.[τ].

without depending on confluence, maybe i can be don in steps,
I already have:

    Σ ⊢ t ≅ t' ->
    Σ ⊢ t .[σ] ≅ t'.[σ].

I can try:

    Σ ⊢ σ ≅ₛ τ ->
    Σ ⊢ t .[σ] ≅ t.[τ].

And maybe I can try to both somehow (using transitivity of conversion or something...)

So that is the other option I have, and in fairness it sounds simpler (less intrusive) than converting exists to dependent sums.

walker (Mar 12 2024 at 12:53):

I am just thinking out loud but also open for suggestions

walker (Mar 12 2024 at 14:42):

walker said:

the other approach which I didn't explore deeply is to just try to do

    Σ ⊢ t ≅ t' ->
    Σ ⊢ σ ≅ₛ τ ->
    Σ ⊢ t .[σ] ≅ t'.[τ].

without depending on confluence, maybe i can be don in steps,
I already have:

    Σ ⊢ t ≅ t' ->
    Σ ⊢ t .[σ] ≅ t'.[σ].

I can try:

    Σ ⊢ σ ≅ₛ τ ->
    Σ ⊢ t .[σ] ≅ t.[τ].

And maybe I can try to both somehow (using transitivity of conversion or something...)

So that is the other option I have, and in fairness it sounds simpler (less intrusive) than converting exists to dependent sums.

@Gaëtan Gilbert It is very very funny ... I just did it exactly like that, all it took is just is just you to confirm that there is no other way to case analyse the ex. It is really funny that manytimes all it takes is someone to confirm that something is doable or not doable for me to do it.

Thanks a lot for the advice :sweat_smile:, you saved me many days of fighting my proof

Last updated: Oct 13 2024 at 01:02 UTC