How to prove something that cannot be created?

Stream: new members

[Chiyoku]

How to prove that something cannot be created? I Asked something similar today because of a problem with by cases x that could not solve the equation x :: xs = List.append a✝ a'✝ and even trying to find another ways to do it, I don't think I understand it enough. There are ways to prove this thing? How should I prove something that I cant construct? I was tried to prove something like this:

inductive Ex where
  | a : Ex
  | c : Ex -> Ex -> Ex

inductive Wot : List σ -> Ex → Type where
  | be  : Wot a b -> Wot a' b' -> Wot (a ++ a') (Ex.c b b')

example : ∀ {x: σ} {xs: List σ}, (Wot (x :: xs) Ex.a) -> Int

[Chris B]

Can you just generalize over the list?

example : ∀ {xs: List σ}, Wot xs Ex.a → Int
| _, w => by cases w; done

[Chris B]

The general problem of "proving something that can't be created" isn't that hard, but having these detailed type indices raises the stakes.

[Chris B]

Similar to what I mentioned in the other thread, you can also use an additional equality hypothesis:

example (hL : L = x :: xs) (hE : E = Ex.a) : Wot L E → Int
| Wot.be h1 h2 => False.elim (Ex.noConfusion hE)