CODEWITHSUNDEEP
coqtheorem-proving
daniel gratzer
daniel gratzer

Reputation: 53871

destruct with dependent types

I have several inductive types defined for a compiler that I'm verifying of this form

Inductive types := Int | Char | Symbol | Bool.
Inductive val : types -> Type := 
| T : val Bool
| F : val Bool
| Num : nat -> val Int
...

Inductive exp : types -> Type :=
   | If : forall {t}, val Bool -> exp t -> exp t -> exp t
   etc...

Now this is fine and simplifies a number of things until I try to prove some theorem like

Theorem example : forall t test (b1 b2 : exp t),
    eval (If test b1 b2) = eval b1
    \/ eval (If test b1 b2) = eval b2.

Now I'd like to do trivial case analysis using destruct test since there are only 2 cases, T and F to consider. But if I attempt this I'd get an error informing me that the destruct tactic generates ill-typed terms. Which it does.

Is there any tactic similar to destruct that will let me do the case analysis on well-typed terms and automatically dispatch those that would be ill-typed? I suspect this is impossible in which case, what would be the correct approach for dealing with proofs of this sort?

Upvotes: 2

Views: 460

Answers (1)

Ptival
Ptival

Reputation: 9437

Since you don't provide your code, I will not try to make sure this works, but the gist of it is to do a dependent inversion, passing the type that should be used:

dependent inversion test with (
  fun t v =>
  match t as _t return val _t -> Prop with
  | Bool => fun v => eval (If v b1 b2) = eval b1 \/ eval (If v b1 b2) = eval b2
  | _    => fun v => False
  end v
).

This is basically equivalent to writing your own dependent pattern matching in such a way that the thing in the with clause up there is your return annotation.

It is somewhat equivalent to doing that:

refine (
  match test as _test in val _t return
    match _t as __t return val __t -> Prop with
    | Bool => fun test => eval (If test b1 b2) = eval b1 \/ eval (If test b1 b2) = eval b2
    | _    => fun _    => _t = Bool -> False
    end _test
  with
  | T => _
  | F => _
  | _ => _
  end
); try discriminate.

Upvotes: 2

Related Questions