# problem with unification

I've faced a problem. I'm not sure how to explain it, so, that is why I'm asking.


Definition sumT (A B : Type) := {x : bool & if x then A else B}.

Definition ind_sum1 {A B}
: forall (C : sumT A B -> Type),
(forall (x : bool) (a : if x then A else B), x = true -> C (existT _ x a)) ->
(forall (x : bool) (b : if x then A else B), x = false -> C (existT _ x b)) ->
forall x : sumT A B, C x :=
fun C fa fb s =>
match s with
| existT _ x v as s' =>
(match x as x' return x = x' -> C s' with
| true => fun ex => fa x v ex
| false => fun ex => fb x v ex
end eq_refl)
end.

Definition ind_sum {A B}
: forall (C : sumT A B -> Type),
(forall a:A, C (existT _ true a)) ->
(forall b:B, C (existT _ false b)) ->
forall x : sumT A B, C x :=
fun C fa fb s =>
(@ind_sum1 A B C
(fun x a eqx => fa (let 'eq_refl := eqx in a))
(fun x b eqx => (let 'eq_refl := eqx in fb b))
s).




In environment
A : Type
B : Type
C : sumT A B -> Type
fa : forall a : A, C (existT (fun x : bool => if x then A else B) true a)
fb : forall b : B, C (existT (fun x : bool => if x then A else B) false b)
s : sumT A B
x : bool
a : if x then A else B
eqx : x = true
The term "a" has type "if x then A else B" while it is expected to have type
"if x then A else ?T" (cannot instantiate "?T" because "B" is not in its scope).



And this is what I do not understand: what is wrong with B? It looks to me like B is actually in the scope. I think this might be one of those cryptic error messages. But how to fix code then?

Answer can be either a good explanation of error or fix the code of ind_sum using ind_sum1 or code of ind_sum without using ind_sum1 (but in programming mode, no tactics).

UPDATE.

Resulting code of ind_sum is


Lemma x_true_x_false_False {x} : x = true -> x = false -> False.
Proof.
intros Ht Hf.
rewrite Ht in Hf.
discriminate Hf.
Qed.

Definition ind_sum {A B}
: forall (C : sumT A B -> Type),
(forall a:A, C (existT _ true a)) ->
(forall b:B, C (existT _ false b)) ->
forall x : sumT A B, C x :=
fun C fa fb s =>
(@ind_sum1 A B C
(fun x eqx a =>
(if x as x' return x = x' -> forall (a : if x' then A else B), (C (existT _ x' a))
then fun eqx' a' => fa a'
else fun eqx' _ => False_rect _ (x_true_x_false_False eqx eqx'))
eq_refl a)
(fun x eqx b =>
(if x as x' return x = x' -> forall (b : if x' then A else B), (C (existT _ x' b))
then fun eqx' _ => False_rect _ (x_true_x_false_False eqx' eqx)
else fun eqx' b' => fb b')
eq_refl b)
s).



Thanks again to Andrej Bauer for the advice!

• Do you know where ?T is created?
– Trebor
Nov 17 at 12:52
• @Trebor, no, I'm not sure I understand where is it created. Code above is as it is, no additional requirements. Nov 17 at 13:05
• Note that the error message does not say the scope, as you wrote, but actually its scope. Hence you need to understand where ?T is created, in order to understand why B is not in its scope.
– Trebor
Nov 17 at 13:06
• good point, thank you. I will try to check the match expression (from the let). Nov 17 at 13:08
• @Trebor, no, unfortunatelly, I 'm not able to see where this ?T is created. any ideas how to know it? Nov 17 at 14:18

I am not quite sure how to fix your code with bare hands, it's going to take a Frenchman to do that, but I can tell you how I would solve this problem: by switching to tactic mode, getting it done, and then inspecting the result. So here we go:

Definition sumT (A B : Type) := {x : bool & if x then A else B}.

Definition ind_sum1 {A B}
: forall (C : sumT A B -> Type),
(forall (x : bool) (a : if x then A else B), x = true -> C (existT _ x a)) ->
(forall (x : bool) (b : if x then A else B), x = false -> C (existT _ x b)) ->
forall x : sumT A B, C x :=
fun C fa fb s =>
match s with
| existT _ x v as s' =>
(match x as x' return x = x' -> C s' with
| true => fun ex => fa x v ex
| false => fun ex => fb x v ex
end eq_refl)
end.

Definition ind_sum {A B}
: forall (C : sumT A B -> Type),
(forall a:A, C (existT _ true a)) ->
(forall b:B, C (existT _ false b)) ->
forall x : sumT A B, C x.


Up to here the code is the same. Now we proceed interactively:

Proof.
intros C fa fb s.
destruct s as [[|] ?]. (* cross fingers *)
- apply fa.
- apply fb.
Defined.


Let us see what Coq came up with. The command Print ind_sum. gives:

ind_sum =
fun (A B : Type) (C : sumT A B -> Type) (fa : forall a : A, C (existT (fun x : bool => if x then A else B) true a))
(fb : forall b : B, C (existT (fun x : bool => if x then A else B) false b)) (s : sumT A B) =>
let (x, y) as s0 return (C s0) := s in
(fun x0 : bool =>
if x0 as b return (forall y0 : if b then A else B, C (existT (fun x1 : bool => if x1 then A else B) b y0))
then fun y0 : A => fa y0
else fun y0 : B => fb y0) x y
: forall (A B : Type) (C : sumT A B -> Type),
(forall a : A, C (existT (fun x : bool => if x then A else B) true a)) ->
(forall b : B, C (existT (fun x : bool => if x then A else B) false b)) -> forall x : sumT A B, C x

Arguments ind_sum {A B}%type_scope (C _ _)%function_scope x


You can now massage the definition given by Coq.

By the way, you might be suffering from boolean blindness. The idiomatic solution is

Inductive sumT (A B : Type) :=
| inl : A -> sumT A B
| inr : B -> sumT A B.

Arguments inl {_} {_} _.
Arguments inr {_} {_} _.

Definition ind_sum {A B}
: forall (C : sumT A B -> Type),
(forall a : A, C (inl a)) ->
(forall b : B, C (inr b)) ->
forall x : sumT A B, C x :=
fun C fa fb x =>
match x with
| inl a => fa a
| inr b => fb b
end.


(And Coq already generates ind_sum for you, it's called sumT_rec (and it's more general than ind_sum.)

• Indeed... Just great! Thank you very much @AndrejBauer Nov 18 at 11:05