avec destruct types dépendants

Question

J'ai plusieurs types inductifs définis pour un compilateur que je suis vérification de ce formulaire

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... 

Maintenant cela est bien beau et simplifie un certain nombre de choses jusqu'à ce que j'essaie de prouver un certain théorème comme

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

maintenant, je voudrais faire une analyse de cas trivial en utilisant destruct test car il n'y a que 2 cas, T et F à considérer. Mais si j'essaie cela, j'obtiendrais une erreur m'informant que la tactique destruct génère des termes mal typés. Ce qu'il fait.

Y a-t-il une tactique similaire à destruct qui me permettra de faire l'analyse de cas sur des termes bien typés et d'envoyer automatiquement ceux qui seraient mal typés? Je soupçonne que c'est impossible dans quel cas, quelle serait la bonne approche pour traiter des preuves de ce genre?

Answer 1

Puisque vous ne fournissez pas votre code, je ne vais pas essayer de vous assurer que cela fonctionne, mais l'essentiel de celui-ci est de faire une inversion dépendante, en passant du type qui doit être utilisé:

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 
). 

Ceci équivaut fondamentalement à écrire votre propre correspondance de motif dépendante de telle sorte que la chose dans la clause with là-haut soit votre annotation de retour.

Il est un peu l'équivalent de le faire:

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.