Stream: Coq users

Topic: case analysis on ex fails


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip walker (Mar 12 2024 at 11:56):

copy paste error, corrected!

view this post on Zulip Gaëtan Gilbert (Mar 12 2024 at 11:57):

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

view this post on Zulip 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 ?

view this post on Zulip Gaëtan Gilbert (Mar 12 2024 at 11:59):

Inductive Term : Type :=
| A.

Check Term : Prop.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Claude Stolze (Mar 12 2024 at 12:10):

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

view this post on Zulip walker (Mar 12 2024 at 12:12):

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

view this post on Zulip Gaëtan Gilbert (Mar 12 2024 at 12:17):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 12 2024 at 12:28):

worry is useless when you have no choice

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip walker (Mar 12 2024 at 12:53):

I am just thinking out loud but also open for suggestions

view this post on Zulip 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: Jun 13 2024 at 19:02 UTC