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?

I don't understand, your example already has `Inductive Term : Set`

what is the code that works?

copy paste error, corrected!

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

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 ?

```
Inductive Term : Type :=
| A.
Check Term : Prop.
```

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

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

right?

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

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.

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

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

basically the whole point of using `exists`

is that there is no other way

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

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

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

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

worry is useless when you have no choice

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.

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

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

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

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.

I am just thinking out loud but also open for suggestions

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