have trouble finding motive of recursion

Stream: new members

[Xiang Li]

I defined an inductive type foo and proved bar1, but I want to know the motive for recursion in the prove, so I write bar2, using @foo.rec_on. Then I can't finish the proof.

universes u v

inductive foo {α : Sort u} {β : Sort v} (a : α) (b : β) : α → β → Sort (max u v)
| mk (s : α) (t : β) : foo s t

lemma bar1 {α β: Type*} {a s : α} {b t : β} (c : foo a b s t) : c = foo.mk s t :=
foo.rec_on c (λ s t, rfl)

lemma bar2 {α β: Type*} {a s : α} {b t : β} (c : foo a b s t) : c = foo.mk s t :=
(@foo.rec_on α β a b (λ a_1 b_1 c_1, a_1 = s → b_1 = t → c_1 == foo.mk s t) s t c (λ m n h1 h2, sorry)) rfl rfl c

[Kyle Miller]

One trick to get the motive out of the bar1 example is

lemma bar1 {α β: Type*} {a s : α} {b t : β} (c : foo a b s t) : c = foo.mk s t :=
foo.rec (λ s t, rfl) c

set_option pp.implicit true
#print bar1

(I'm not sure why I had to change foo.rec_on to foo.rec for it to honor the pp.implicit option.) After some manipulation of the printed expression, I got

theorem bar3 {α : Type*} {β : Type*} {a s : α} {b t : β} (c : foo a b s t): c = foo.mk s t :=
  @foo.rec_on α β a b (λ (a' : α) (b' : β) (c' : foo a b a' b'), c' = foo.mk a' b') s t
  c (λ (s : α) (t : β), rfl)

[Xiang Li]

Thank you very much! :+1: