Comment prouver que l'ajout d'une nouvelle variable à l'expression ne change pas sa sémantique?

Question

Voici un langage très simple:

type_synonym vname = "string" 
type_synonym bool3 = "bool option" 
type_synonym env = "vname ⇒ bool3" 

datatype exp = Let vname bool exp | Var vname | And exp exp 

primrec val :: "exp ⇒ env ⇒ bool3" where 
    "val (Let var init body) e = val body (e(var ↦ init))" 
| "val (Var var) e = e var" 
| "val (And a b) e = (case (val a e, val b e) of 
    (Some x, Some y) ⇒ Some (x ∧ y) | _ ⇒ None)" 

Je suis en train de prouver que si l'expression n'a pas de variables libres, je peux déclarer toute nouvelle variable au début de l'expression. J'ai essayé 3 approches pour le prouver.

1) defined fonction vérifie si la valeur de l'expression est bien définie (= toutes les variables utilisées sont déclarées):

primrec defined :: "exp ⇒ env ⇒ bool" where 
    "defined (Let var init body) e = defined body (e(var ↦ init))" 
| "defined (Var var) e = (var : dom e)" 
| "defined (And a b) e = (defined a e ∧ defined b e)" 

lemma var_intro: "defined exp env ⟹ defined exp (env(x ↦ init))" 
    apply (induct exp) 
    apply (simp_all split: if_splits) 

2) L'approche alternative est de collecter toutes les variables libres de l'expression. Et si l'expression ne contient pas alors nous pouvons ajouter une nouvelle variable à l'environnement:

primrec freeVars :: "exp ⇒ vname set ⇒ vname set" where 
    "freeVars (Let var init body) e = freeVars body (insert var e)" 
| "freeVars (Var var) e = (if var ∈ e then {} else {var})" 
| "freeVars (And a b) e = freeVars a e ∪ freeVars b e" 

lemma var_intro2: "freeVars exp {} = {} ⟹ freeVars exp {x} = {}" 
    apply (induct exp) 
    apply (simp_all split: if_splits) 

3) Et la dernière approche est d'éliminer toutes les variables bornées de l'environnement:

primrec isFree :: "vname ⇒ exp ⇒ bool" where 
    "isFree x (Let var init body) = (if var = x then False else isFree x body)" 
| "isFree x (Var var) = (var = x)" 
| "isFree x (And a b) = (isFree x a ∨ isFree x b)" 

lemma var_elim: "¬ isFree x exp ⟹ val exp (env(x ↦ init)) = val exp (env)" 
    apply (induct exp) 
    apply (simp_all split: if_splits) 

Je ne peux prouver aucun des lemmes. Pourriez-vous suggérer une solution?

Answer 1

Vos preuves, il faudra probablement vous de définir env à arbitrary dans l'induction ou les preuves ne fonctionnera pas. Avec cela, vous serez probablement capable de prouver les propriétés que vous avez indiquées, mais je pense que ce sera un peu moche parce que vos définitions et vos déclarations de lemme sont inutilement spécifiques, ce qui peut rendre les preuves plus douloureuses.

En particulier, votre notion de «variable libre w.r.t. un environnement me semble un peu inutilement compliqué. Je pense qu'il est plus facile d'utiliser les éléments suivants:

primrec freeVars :: "exp ⇒ vname set" where 
    "freeVars (Let var init body) = freeVars body - {var}" 
| "freeVars (Var var) = {var}" 
| "freeVars (And a b) = freeVars a ∪ freeVars b" 

La déclaration « expression exp est w.r.t. bien défini un environnement env 'est alors simplement freeVars exp ⊆ dom env.

Ensuite, il est évident que toute expression qui est bien définie w.r.t. certains environnements sont également bien définis avec un environnement plus vaste.

Answer 2

1) Vous devez lever la propriété communicative de l'insertion d'élément sur les ensembles dans celle des mises à jour d'état sur les cartes, sur lesquelles votre lemme est basé.

lemma defined_dom: "defined exp env ⟹ dom env = dom env' ⟹ defined exp env'" 
    by (induction exp arbitrary: env env'; auto) 
lemma defined_comm: "defined exp (env(x↦a, y↦b)) ⟹ defined exp (env(y↦b, x↦a))" 
    by (auto elim!: defined_dom) 
lemma var_intro: "defined exp env ⟹ defined exp (env(x ↦ init))" 
    by (induction exp arbitrary: env; simp add: defined_comm) 

2) Si votre lemme est basé sur des ensembles, vous aurez également besoin du lemme communicatif, qui est déjà dans la bibliothèque:

lemma var_intro2': "freeVars exp s = {} ⟹ freeVars exp (insert x s) = {}" 
by (induction exp arbitrary: s x; force simp: insert_commute) 
lemma var_intro2: "freeVars exp {} = {} ⟹ freeVars exp {x} = {}" 
    using var_intro2' . 

3) De même:

lemma var_elim: "¬ isFree x exp ⟹ val exp (env(x ↦ init)) = val exp (env)" 
    by (induction exp arbitrary: env; simp add: fun_upd_twist split: if_splits)