Chantal Keller (Jun 09 2021 at 15:44): 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!
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.
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 .
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).
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
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?
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.
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)
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
Gaëtan Gilbert (Oct 21 2021 at 16:56):it is not @eq bool which matters but rather @eq Type bool
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.
@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)
Valentin Blot (Oct 21 2021 at 21:09):Nice, thanks both of you!
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
probably
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?
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: Sep 30 2023 at 05:01 UTC