Hi

I have the following piece of code:

```
Require Import Bool.
Inductive depInd : Type -> Type :=
| A : depInd bool
| B : depInd unit.
Definition foo : forall (a : Type) (D : depInd (id a)),
a -> bool :=
fun a D => match D with
| A => fun x => eqb true x
| B => fun _ => true
end.
Definition bar_ok : forall (a : Type) (D : depInd a),
(match D with
| A => bool
| B => unit
end) -> bool :=
fun a D => match D with
| A => fun x => eqb true x
| B => fun _ => true
end.
Fail Definition bar_ko : forall (a : Type) (D : depInd (id a)),
(match D with
| A => bool
| B => unit
end) -> bool :=
fun a D => match D with
| A => fun x => eqb true x
| B => fun _ => true
end.
```

I do not get why the definition of `foo`

goes through, but not the definition of `bar_ko`

. I expected this latter not to rely on an inversion on the type of `D`

. Could you explain the mechanism?

Thanks!

I am not sure to understand what your issue is. But it has to be said that the inference of return clauses is fullchoke of heuristics. One heuristic triggers for `foo`

, a different one triggers for `bar_ok`

, and for `bar_ko`

, Coq is confused about which one to use.

Coq is not very clever in figuring out how the types of each branch of the `match`

depend on the discriminee (you can `Print bar_ok`

to see the actual gallina code that was generated in your working example). It's usually necessary to annotate the match construct explaining the dependencies, e.g. by moving the return type of the match in the `return`

keyword.

```
Definition bar_ok2 :=
fun (a : Type) (D : depInd (id a)) =>
match
D as D0
return (match D0 with
| A => bool
| B => unit
end -> bool)
with
| A => fun x => eqb true x
| B => fun _ => true
end .
```

The `as`

keyword allows you to refer to the discriminee "within" each branch, after matching (have a look at the gallina code that's generated for each branch of `bar_ok2`

).

Even simpler is to have it depend on the index directly using the `in`

keyword to match on the type with its index:

```
Definition bar_ok3 :=
fun (a : Type) (D : depInd (id a)) =>
match
D in depInd t
return t -> bool
with
| A => fun x => eqb true x
| B => fun _ => true
end .
```

Thank you very much for your answers! `bar_ok2`

is what I expected: there is a way not to inspect the type of `D`

. I indeed did not try to use `return`

to make it explicit in the body (in addition to the type).

Coq sadly prefers to try its heuristics even if you really passed the type constraint by ascribing a type to bar_ok... `return`

and `in`

are indeed the way to disable the heuristics

Hi

I am refreshing this thread since I have a new question on the same type. In the following, is it possible to prove `depInd_bool`

without axioms?

```
Require Coq.Program.Equality.
Inductive depInd : Type -> Type :=
| A : depInd bool
| B : depInd unit.
Lemma elim_unit_bool : @eq Type unit bool -> False.
Proof.
intro H.
assert (H1:forall (x y:bool), x = y).
{ rewrite <- H. now intros [] []. }
assert (H2:=H1 true false). inversion H2.
Qed.
Module WithAxioms.
Import Coq.Program.Equality.
Lemma depInd_bool : forall (x:depInd bool), x = A.
Proof.
intro x. dependent induction x.
- reflexivity.
- elim (elim_unit_bool x1).
Qed.
Print Assumptions depInd_bool.
End WithAxioms.
```

Or to prove that `depInd`

has a decidable equality?

Since `bool`

has decidable equality, `@eq bool`

satisfies UIP; the `dependent induction`

tactic from Equations should be able to use this automatically.

IIRC, Equations can even prove decidable equality for `depInd T`

automatically — I've hit scaling issues but on much larger examples (6 mutual inductives, ~30-40 constructors)

depind is isomorphic to

```
Inductive depInd' (T:Type) : Type :=
| A' (_:T = bool)
| B' (_:T = unit).
```

then `depInd bool`

is isomorphic to `bool = bool`

but with univalence this has 2 elements

it is not `@eq bool`

which matters but rather `@eq Type bool`

Thanks Gaëtan, following your remark I tried but didn't succeed in proving the isomorphism:

```
Inductive depInd : Type -> Type :=
| A : depInd bool
| B : depInd unit.
Inductive depInd' (T:Type) : Type :=
| A' : T = bool -> depInd' T
| B' : T = unit -> depInd' T.
Definition f {T : Type} (x : depInd T) : depInd' T :=
match x with
| A => A' bool eq_refl
| B => B' unit eq_refl
end.
Import EqNotations.
Definition g {T : Type} (x : depInd' T) : depInd T :=
match x with
| A' _ H => rew <- H in A
| B' _ H => rew <- H in B
end.
Lemma gf (T : Type) : forall x : depInd T, g (f x) = x.
intro x; destruct x; reflexivity.
Qed.
Lemma fg (T : Type) : forall x : depInd' T, f (g x) = x.
```

@Valentin Blot you need a bit of dependent pattern-matching, here is a reasonably simple proof of the iso:

```
Definition eq_sym {A : Type} {x y : A} (e : x = y) : y = x.
Proof.
destruct e.
reflexivity.
Defined.
Lemma sym_sym : forall A (x y : A) (e : x = y), eq_sym (eq_sym e) = e.
Proof.
destruct e.
reflexivity.
Defined.
Lemma fg (T : Type) : forall x : depInd' T, f (g x) = x.
Proof.
induction x; simpl.
+ rewrite <- (sym_sym _ _ _ e).
refine (
match eq_sym e as e₀ in _ = U return f (rew <- [depInd] (eq_sym e₀) in A) = A' U (eq_sym e₀)
with
eq_refl => _
end).
reflexivity.
+ rewrite <- (sym_sym _ _ _ e).
refine (
match eq_sym e as e₀ in _ = U return f (rew <- [depInd] (eq_sym e₀) in B) = B' U (eq_sym e₀)
with
eq_refl => _
end).
reflexivity.
Qed.
```

It turns out `destruct`

is clever enough, so the following is enough (with the two lemmas above)

```
Lemma fg (T : Type) : forall x : depInd' T, f (g x) = x.
Proof.
induction x; simpl.
+ rewrite <- (sym_sym _ _ _ e).
destruct (eq_sym e).
reflexivity.
+ rewrite <- (sym_sym _ _ _ e).
destruct (eq_sym e).
reflexivity.
Qed.
```

if you're willing to change the spec a bit you can do simply

```
Inductive depInd : Type -> Type :=
| A : depInd bool
| B : depInd unit.
Inductive depInd' (T:Type) : Type :=
| A' : bool = T :> Type -> depInd' T
| B' : unit = T :> Type -> depInd' T.
Definition f {T : Type} (x : depInd T) : depInd' T :=
match x with
| A => A' bool eq_refl
| B => B' unit eq_refl
end.
Import EqNotations.
Definition g {T : Type} (x : depInd' T) : depInd T :=
match x with
| A' _ H => rew H in A
| B' _ H => rew H in B
end.
Lemma gf (T : Type) : forall x : depInd T, g (f x) = x.
intro x; destruct x; reflexivity.
Qed.
Lemma fg (T : Type) : forall x : depInd' T, f (g x) = x.
Proof.
intros x;destruct x as [[]|[]];reflexivity.
Qed.
```

(the equations were changed from `T = bool`

to `bool = T :> Type`

because we can destruct proofs of equalities when the right hand side is a variable, and the `:> Type`

is to deal with stupid Type vs Set issues)

Nice, thanks both of you!

Got it:

```
Inductive depInd : Set -> Set :=
| A : depInd bool
| B : depInd unit.
Definition bla := (fun e : bool = bool => eq_rect bool depInd A bool e) : bool = bool -> depInd bool.
```

and then if I give to `bla`

the equality coming from univalence on the negation on `bool`

, I get another inhabitant of `depInd bool`

.

subsidiary question : can I prove the following?

```
(forall (x : depInd bool), x = A) -> forall (e : bool = bool), e = eq_refl
```

probably

Stupid question: does that mean that we cannot add an indexed HIT depInd, where we make depInd bool a singleton via an extra path constructor?

Answering my own question, yes we can:

```
Set Keep Proof Equalities.
Goal (forall (x : depInd bool), x = A) -> forall e : @eq Type bool bool, e = eq_refl.
intro H.
assert (H' : forall x : depInd' bool, x = A' bool eq_refl).
intro x.
rewrite <- (fg _ x), <- (fg _ (A' _ _)).
f_equal.
simpl.
apply H.
intro e.
cut (A' bool e = A' bool eq_refl).
intro He.
injection He.
exact (fun x => x).
apply H'.
Qed.
```

Last updated: Sep 30 2023 at 05:01 UTC