Extracting a proof from an inductively defined Prop

Stream: new members

[Z. Wu]

I have the following code, where the component of TransCompose is constructed with some state sa1, sa2, their properties ta and ha.
Now in extractEq₀, I want to extract ha from an instance of TransCompose using match.

variable {α Io: Type}
variable {genProp: Io -> Prop}
variable (R₁: α->α->Prop)

inductive TransCompose
  (getR₁Io: (s s':α) -> R₁ s s' -> Io)
  : α -> α -> Prop  where
| TransPara sa1 sa2 (ta: R₁ sa1 sa2)
    (ha: genProp (getR₁Io sa1 sa2 ta)):
      TransCompose getR₁Io sa1 sa2

variable (getR₁Io: (s s': α) -> R₁ s s' -> Io)

def extractEq₀
  (x x': α)
  (tn: @TransCompose α Io genProp R₁ getR₁Io x x') :=
  match tn with
  | .TransPara _ _ ta ha => ha

However, the aforementioned code won't work, with the following error message on the last line:

type mistmatch, alternative has type
  genProp (getR₁Io x x' ta) : Prop
but is expected to have type
  ?m.200 x x' (_ : TransCompose R₁ getR₁Io x x') : Sort ?u.198

It seems that lean cannot figure out the actual type of ha, and my guess is that it is a result of ha depending on ta, which is embed in the inductive constructor. It is however confusing that I can use the same code to extract ta (replace =>ha with =>ta). So I'm not sure what is fundamentally different between ta and ha.
Also, I'm wondering what I can do to extract the proof ha. thanks!

[Z. Wu]

Ok, I tried to roll my custom motive, and it seems working as the type I want:

def motive (x x': α) (t: @TransCompose α Io genProp R₁ f x x') :=
  let ta := match t with
  | .TransPara _ _ ta _ => ta
  genProp (f x x' ta)


def extractEq₁
  (x x': α)
  (tn: @TransCompose α Io genProp R₁ getR₁Io x x') :=
  @TransCompose.casesOn α Io genProp R₁ getR₁Io x x' (motive R₁ x x') tn (fun ta ha => ha)

And it seems that if I let lean derive the motive, it essentially gives similar, if not the same, message:

def extractEq₁'
  (x x': α)
  (tn: @TransCompose α Io genProp R₁ getR₁Io x x') :=
  @TransCompose.casesOn α Io genProp R₁ getR₁Io x x' _ tn (fun ta ha => ha)
/-
type mismatch
  ha
has type
  genProp (getR₁Io x x' ta) : Prop
but is expected to have type
  ?m.468 x x' tn (_ : TransCompose R₁ getR₁Io x x') : Sort ?u.459
-/

But I'm still not so sure what is preventing me from using match. This would be quite tedious to work with.

[Shreyas Srinivas]

I don't you can match on proofs. Someone who feels more confident about their type theory than me can explain the why, but it boils down to there being no distinction between two proofs of the same prop.

[Riccardo Brasca]

You can.

example (P Q R : Prop) (x : P ∨ Q) : R := match x with
| Or.inl p => sorry
| Or.inr q => sorry

works. But the proposition must be an inductively defined proposition, and it eliminates only to Prop (unless it is a syntactic subsingleton)

[Z. Wu]

Yeah, I agree that something has to do with proof irrelevance here. IIRC, practically this means that I can have functions transforming Prop to Prop, or Type to Prop, but not Prop to Type. This limitation is in someway enforced in the casesOn/recOn signatures for inductively defined Prop.

In my example, I'm indeed trying to transform a Prop (the destructed TransCompose) to another Prop (the genProp (...)). So to me this should be valid, and the manually provided motive/ extractEq₁ also shows that this transformation is ok (if my motive is correct...)

I'm wondering ways where I can make match work, so I don't have to write motive. :)