Writing a well founded relation for a proposition

Stream: lean4

[Plecra]

abbrev size_of_deriv (derivation : BlendedDerivation g r s) :=
  match derivation with
  | .Terminal => 0
  | .Rule _ _ xs => 1 + size_of_deriv xs
  | .Concat a b => 1 + size_of_deriv a + size_of_deriv b

Is there a way to write a function that I can use with termination_by like this, where BlendedDerivation is in Prop

[Henrik Böving]

Propositions cannot eliminate into non-propositional things so no.

[Plecra]

sure, but presumably termination_by could be fine with a well-founded measure in Prop?

[Henrik Böving]

Of course, you can for example use fun _ => 0 or something like that. But you cannot perform pattern matching on your Prop when you want to produce non-Prop data.

[Henrik Böving]

(deleted)

[Henrik Böving]

(deleted)

[Henrik Böving]

(Forget what I said that just looks like it achieves what you want)

[Plecra]

I cant quite tell what you mean with fun _ => 0 there :) What can I use it for?

[Plecra]

The couple ways I tried to write it, it still belongs in Type

[Henrik Böving]

You can in principle use that as a measure for a Prop thing but that's of course a very boring measure.

[Plecra]

Then I guess I'm just asking my original question ^^ I have an inductive type:

inductive BlendedDerivation : Grammar -> Rule -> Text -> Prop where
| Terminal : BlendedDerivation g [(.Terminal s)] s
| Rule : MemberAt g rules n
  -> rule ∈ rules
  -> BlendedDerivation g rule s
  -> BlendedDerivation g [(.NonTerminal n)] s
| Concat : BlendedDerivation g a s1 -> BlendedDerivation g b s2 -> BlendedDerivation g (a ++ b) (s1 ++ s2)

and I want to use the wf relation between the constructors that I wrote above, but I want to do it without putting BlendedDerivation into Type. This seems pretty sensible in the abstract, in that we never actually need to eliminate out of the termination measure

[Plecra]

alternatively, how can I prove extension_preserves_deriv_ when BlendedDerivation g r t is in Prop https://pastebin.com/raw/sP4gdzw0

[Floris van Doorn]

Style comment: please put your Lean code in #backticks (and if you want us to be able to run the code, write a #mwe)

[Michael Rothgang]

Doing so makes it much easier to help you - i.e. is nicer for everybody :-)

[Vlad]

While one would typically proceed by induction on deriv : BlendedDerivation g r s, here the elaborator proves termination automatically:

abbrev Text := List UInt8
inductive Pattern where
| Terminal : Text -> Pattern
| NonTerminal : Nat -> Pattern
abbrev Rule := List Pattern
abbrev Grammar := List <| List Rule

inductive MemberAt : List a -> a -> Nat -> Prop where
| Here : MemberAt (x::xs) x 0
| There : MemberAt xs v n -> MemberAt (x::xs) v (n + 1)

inductive BlendedDerivation : Grammar -> Rule -> Text -> Prop where
| Terminal : BlendedDerivation g [(.Terminal s)] s
| Rule : MemberAt g rules n
  -> rule ∈ rules
  -> BlendedDerivation g rule s
  -> BlendedDerivation g [(.NonTerminal n)] s
| Cons : BlendedDerivation g [p] s1 -> BlendedDerivation g b s2 -> BlendedDerivation g (p::b) (s1 ++ s2)

theorem extension_preserves_member_loc : MemberAt l v n -> MemberAt (l ++ ls) v n := by
  induction l generalizing n
  intro hk
  cases hk
  next h t ih =>
  intro hk
  cases hk
  apply MemberAt.Here
  apply MemberAt.There
  next childh =>
  specialize ih childh
  assumption

inductive InGrammar : Grammar -> Rule -> Text -> Prop where
| Via : BlendedDerivation g r s -> InGrammar g r s

theorem extension_preserves_deriv_ (deriv : BlendedDerivation g r s) : BlendedDerivation (g ++ g2) r s :=
  match deriv with
  | .Terminal =>
    BlendedDerivation.Terminal
  | .Rule rules_mem rule_mem rule_has_s =>
    BlendedDerivation.Rule (extension_preserves_member_loc rules_mem) rule_mem (extension_preserves_deriv_ rule_has_s)
  | .Cons hleft hright =>
    by
      apply BlendedDerivation.Cons
      exact extension_preserves_deriv_ hleft
      exact extension_preserves_deriv_ hright

theorem extension_preserves_deriv (p : InGrammar g r s) : InGrammar (g ++ g2) r s :=
  by
    cases p
    apply InGrammar.Via
    apply extension_preserves_deriv_
    assumption

[Vlad]

For terms in Prop, theorem is preferred over def.