Pattern Matching or Induction on Lattice?

Stream: new members

[AHan]

If I have a type which is an instance of lattice, how can I pattern match or do induction on it?
For example,

import data.set.lattice
open lattice
variables {α : Type*} [semilattice_sup_bot α]
lemma x (p : α → β) :  ∀ (a : α), p a
| a :=

[Johan Commelin]

@AHan Why are you trying to do?

[Johan Commelin]

Pattern matching doesn't work on any odd type. (This has nothing to do with lattices.) You need α to be inductive.

[AHan]

I want to prove something like

lemma lex_acc_of_bot : ∀ (a b : α) (l : list α), (ra a b) → acc (lex ra) (a :: l) := sorry

[Johan Commelin]

Ok, I don't know enough about this... (I don't know what ra and lex are). But what had you hoped to pattern match on? Whether a was the bottom element, or something like that?

[Johan Commelin]

For your lemma, you could do induction on the list; maybe that helps?

[AHan]

Oh sorry I should say it clearer

inductive lex (r : α → α → Prop) : list α → list α → Prop
| nil {} {a l} : lex [] (a :: l)
| rel {a₁ a₂} (l₁ l₂ : list α) (h₁ : r a₁ a₂) (h₂ : l₁.length ≤ l₂.length) : lex (a₁ :: l₁) (a₂ :: l₂)
| cons {a l₁ l₂} (h : lex l₁ l₂) : lex (a :: l₁) (a :: l₂)

and ra is actually lt

[Kevin Buzzard]

I found Chris' notes on well founded recursion very useful for this sort of thing.

[Kevin Buzzard]

To get the equation compiler to match on a random thing, you need to explicitly trigger it with the match command. Hang on I'll get to a PC and send some links

[AHan]

I have tried to do induction on list
But the lex order I defined doesn't necessarily decrease on the length of the list... I can't apply the induction hypothesis...

[Kevin Buzzard]

https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#match-expressions for pattern matching

https://github.com/leanprover/mathlib/blob/master/docs/extras/well_founded_recursion.md for well-founded recursion

[AHan]

@Kevin Buzzard Thanks a lot for the sharing!
So I think the main problem here is, I have to prove that something will decrease....
And I have no idea how to prove this.... lol