Comment prouver en HOLCF que le double retour d'une liste ne change pas

Question

Voici une simple théorie écrite sur la plaine HOL:

theory ToyList 
    imports Main 
begin 

no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65) 
hide_type list 
hide_const rev 

datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) 

primrec snoc :: "'a list => 'a => 'a list" (infixr "#>" 65) 
    where 
    "[] #> y = y # []" | 
    "(x # xs) #> y = x # (xs #> y)" 

primrec rev :: "'a list => 'a list" 
    where 
    "rev [] = []" | 
    "rev (x # xs) = (rev xs) #> x" 

lemma rev_snoc [simp]: "rev(xs #> y) = y # (rev xs)" 
    apply(induct_tac xs) 
    apply(auto) 
done 

theorem rev_rev [simp]: "rev(rev xs) = xs" 
    apply(induct_tac xs) 
    apply(auto) 
done 

end 

snoc est un opposé de cons. Il ajoute un élément à la fin de la liste.

Je veux prouver un lemme similaire via HOLCF. Dans un premier temps, je ne considère que des listes strictes. J'ai déclaré le domaine des listes strictes dans HOLCF. J'ai aussi déclaré deux fonctions récursives:

• ssnoc - Ajoute un élément à la fin d'une liste
• srev - ANNULE une liste

Prefix s signifie "stricte".

theory Test 
    imports HOLCF 
begin 

domain 'a SList = SNil | SCons "'a" "'a SList" 

fixrec ssnoc :: "'a SList → 'a → 'a SList" 
    where 
    "ssnoc ⋅ SNil ⋅ x = SCons ⋅ x ⋅ SNil" | 
    "ssnoc ⋅ ⊥ ⋅ x = ⊥" | 
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ ssnoc ⋅ (SCons ⋅ x ⋅ xs) ⋅ y = SCons ⋅ x ⋅ (ssnoc ⋅ xs ⋅ y)" 

fixrec srev :: "'a SList → 'a SList" 
    where 
    "srev ⋅ ⊥ = ⊥" | 
    "srev ⋅ SNil = SNil" | 
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ srev ⋅ (SCons ⋅ x ⋅ xs) = ssnoc ⋅ (srev ⋅ xs) ⋅ x" 

lemma srev_singleton [simp]: 
    "srev ⋅ (SCons ⋅ a ⋅ SNil) = SCons ⋅ a ⋅ SNil" 
    apply(induct) 
    apply(simp_all) 
done 

lemma srev_ssnoc [simp]: 
    "srev ⋅ (ssnoc ⋅ xs ⋅ a) = SCons ⋅ a ⋅ (srev ⋅ xs)" 
    apply(induct xs) 
    apply(simp_all) 
done 

lemma srev_srev [simp]: 
    "srev ⋅ (srev ⋅ xs) = xs" 
    apply(induct xs) 
    apply(simp_all) 
done 

end 

Je suis en train de prouver que le double retour de la liste égale à la liste originale (lemme srev_srev). Je l'ai déclaré deux lemmes d'aide:

• srev_singleton - inverse de la liste singleton est la liste singleton originale
• srev_ssnoc - réversion de la liste est égal à la liste à partir du dernier élément de la liste initiale annexant réversion de le reste des éléments de la liste originale

Mais je ne peux pas prouver aucun des lemmes. Pourriez-vous signaler les erreurs?

Pourquoi la condition préalable "x ≠ ⊥ ∧ xs ≠ ⊥" est-elle nécessaire dans les définitions de fonctions? Et pourquoi devrais-je déclarer "srev ⋅ ⊥ = ⊥" et "ssnoc ⋅ ⊥ ⋅ x = ⊥" explicitement. Je suppose que dans HOLCF par défaut, les fonctions sont indéfinies si l'un des arguments est indéfini.

Answer 1

Si votre intention est de modéliser des listes a la Haskell (alias "listes paresseux"), alors vous devriez utiliser quelque chose comme:

domain 'a list = Nil ("[]") | Cons (lazy 'a) (lazy "'a list") (infix ":" 65) 

(notez les annotations "paresseux" pour Cons). Ensuite, vous n'avez pas besoin des hypothèses sur votre troisième équation. Par exemple,

fixrec append :: "'a list → 'a list → 'a list" 
    where 
    "append $ [] $ ys = ys" 
    | "append $ (x : xs) $ ys = x : (append $ xs $ ys)" 

pour ce que vous avez appelé ssnoc et

fixrec reverse :: "'a list → 'a list" 
    where 
    "reverse $ [] = []" 
    | "reverse $ (x : xs) = append $ xs $ (x : [])" 

pour la marche arrière.

Cependant, étant donné que ce type de listes autorise des valeurs "infinies", vous ne pourrez pas prouver que reverse $ (reverse $ xs) = xs est en général (parce que ce n'est pas le cas). Cela ne vaut que pour les listes finies, qui peuvent être caractérisées par induction. (Voir, par exemple, https://arxiv.org/abs/1306.1340 pour une discussion plus détaillée.)

Si, cependant, vous ne voulez pas modéliser les listes paresseuses (c'est-à-dire ne voulez vraiment pas les annotations "paresseuses" dans votre type de données), alors vos équations pourrait ne pas tenir sans les hypothèses. Maintenant, si les équations ont ces hypothèses, elles ne peuvent être appliquées que dans les cas où les hypothèses sont satisfaites.Donc, gain, vous ne serez pas en mesure de prouver (sans hypothèses supplémentaires) que reverse $ (reverse $ xs) = xs. Il pourrait encore être possible d'obtenir les hypothèses appropriées par un prédicat inductif, mais je n'ai pas étudié davantage.

Mise à jour: Après avoir joué un peu avec des listes strictes HOLCF, j'ai quelques commentaires:

D'abord, je suppose que les conditions du cahier des charges fixrec sont nécessaires en raison de la construction interne, mais nous sont capables de se débarrasser d'eux après. J'ai réussi à prouver votre lemme comme suit. Pour être complet, je donne tout le contenu de mon fichier de théorie. Tout d'abord assurez-vous que la notation ne heurte pas existant:

no_notation 
    List.Nil ("[]") and 
    Set.member ("op :") and 
    Set.member ("(_/ : _)" [51, 51] 50) 

Définissez ensuite le type de listes strictes

domain 'a list = Nil ("[]") | Cons 'a "'a list" (infixr ":" 65) 

et la fonction snoc.

fixrec snoc :: "'a list → 'a → 'a list" 
    where 
    "snoc $ [] $ y = y : []" 
    | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ snoc $ (x:xs) $ y = x : snoc $ xs $ y" 

Maintenant, nous obtenons une variante inconditionnelle de la seconde équation par:

1. montrant que snoc est stricte dans son premier argument (notez l'utilisation de fixrec_simp).
2. Montrer que snoc est strict dans son second argument (ici l'induction est nécessaire).
3. Et enfin, d'obtenir l'analyse équation par cas sur les trois variables.

lemma snoc_bot1 [simp]: "snoc $ ⊥ $ y = ⊥" by fixrec_simp 
lemma snoc_bot2 [simp]: "snoc $ xs $ ⊥ = ⊥" by (induct xs) simp_all 
lemma snoc_Cons [simp]: "snoc $ (x:xs) $ y = x : snoc $ xs $ y" 
    by (cases "x = ⊥"; cases "xs = ⊥"; cases "y = ⊥";simp) 

ensuite la fonction reverse

fixrec reverse :: "'a list → 'a list" 
    where 
    "reverse $ [] = []" 
    | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ reverse $ (x : xs) = snoc $ (reverse $ xs) $ x" 

et encore une variante inconditionnelle de sa deuxième équation:

lemma reverse_bot [simp]: "reverse $ ⊥ = ⊥" by fixrec_simp 
lemma reverse_Cons [simp]: "reverse $ (x : xs) = snoc $ (reverse $ xs) $ x" 
    by (cases "x = ⊥"; cases "xs = ⊥"; simp) 

Maintenant le lemme sur les reverse et snoc vous aviez aussi:

lemma reverse_snoc [simp]: "reverse $ (snoc $ xs $ y) = y : reverse $ xs" 
    by (induct xs) simp_all 

Et enfin le lemme désiré:

lemma reverse_reverse [simp]: 
    "reverse $ (reverse $ xs) = xs" 
    by (induct xs) simp_all 

La façon dont j'ai obtenu cette solution était simplement en regardant dans les sous-objectifs restants de vos tentatives infructueuses, puis obtenir plus Failed tentatives, se pencher sur les sous-objectifs restants, répétez, ...