## 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 `Σ ⊢ σ ≅ₛ τ `:

``````     Σ ⊢ σ ≅ₛ τ <->
(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,

``````    Σ ⊢ 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,

``````    Σ ⊢ 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