Say I have a type:
inductive is_sorted {α: Type} [decidable_linear_order α] : list α -> Prop
| is_sorted_zero : is_sorted []
| is_sorted_one : Π (x: α), is_sorted [x]
| is_sorted_many : Π {x y: α} {ys: list α}, x < y -> is_sorted (y::ys) -> is_sorted (x::y::ys)
And it's decidable:
instance decidable_sorted {α: Type} [decidable_linear_order α] : ∀ (l : list α), decidable (is_sorted l)
If I have a particular list:
def l1: list ℕ := [2,3,4,5,16,66]
Is it possible to prove that it's sorted at "compile time"; to produce an is_sorted l1 at the top level?
I've tried def l1_sorted: is_sorted l1 := if H: is_sorted l1 then H else sorry, but I don't know how to show the latter case is impossible. I've also tried the simp tactic but that didn't seem to help.
I can prove it with #reduce, but it doesn't possible to assign the output of that to a variable.
You should be able to use dec_trivial to prove l1_sorted. This will try to infer an instance of decidable (is_sorted l1), and if the instance evaluates to is_true p, it will reduce to p.