Stream: Coq users

Topic: Dependent inductives


view this post on Zulip Chantal Keller (Jun 09 2021 at 15:44):

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!

view this post on Zulip Guillaume Melquiond (Jun 09 2021 at 16:03):

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.

view this post on Zulip spaceloop (Jun 09 2021 at 16:20):

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 .

view this post on Zulip Chantal Keller (Jun 09 2021 at 16:29):

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).

view this post on Zulip Matthieu Sozeau (Jun 10 2021 at 21:18):

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

view this post on Zulip Chantal Keller (Oct 21 2021 at 16:44):

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?

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 16:51):

Since bool has decidable equality, @eq bool satisfies UIP; the dependent induction tactic from Equations should be able to use this automatically.

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 16:52):

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)

view this post on Zulip Gaëtan Gilbert (Oct 21 2021 at 16:55):

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

view this post on Zulip Gaëtan Gilbert (Oct 21 2021 at 16:56):

it is not @eq bool which matters but rather @eq Type bool

view this post on Zulip Valentin Blot (Oct 21 2021 at 20:55):

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.

view this post on Zulip Pierre-Marie Pédrot (Oct 21 2021 at 21:06):

@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.

view this post on Zulip Pierre-Marie Pédrot (Oct 21 2021 at 21:07):

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.

view this post on Zulip Gaëtan Gilbert (Oct 21 2021 at 21:08):

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)

view this post on Zulip Valentin Blot (Oct 21 2021 at 21:09):

Nice, thanks both of you!

view this post on Zulip Valentin Blot (Oct 21 2021 at 21:26):

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

view this post on Zulip Gaëtan Gilbert (Oct 21 2021 at 21:54):

probably

view this post on Zulip Paolo Giarrusso (Oct 22 2021 at 03:12):

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?

view this post on Zulip Valentin Blot (Oct 22 2021 at 07:04):

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: Feb 06 2023 at 12:04 UTC