Personnes présentes
- Romain Aissat
- Thibaut Balabonski
- Frédéric Boulanger
- Chantal Keller
- Yakoub Nemouchi
- Hai Nguyen Van
- Frédéric Tuong
- Burkhart Wolff
- Lina Ye
Problèmes
Thibaut demande comment vérifier une propriété sur une fonction qui n'est pas définie dans tous les cas.
Il faut ajouter la précondition sur l'argument dans les hypothèses de la preuve.
Frédéric B. : différence entre undefined et None.
Burkhart : None est différent de Some x, pour undefined, on sait uniquement que undefined = undefined.
Perles
Burkhart :
Comment modéliser une fonction wot~:
wot [] --> []
wot [s 0] --> wot[s]
wot [a b c n] --> wot [a b c (n-1) (n-1) ... (n-1)] (n-1) fois (n-1)
Pour la terminaison, il faut donner un ordre bien fondé tel que l'appel récursif donne quelque chose de plus petit.
Ordre sur un multiset.
Une théorie des multiset et multiset order est disponible dans la bibliothèque Isabelle (mais pas incluse dans Main)
less_multiset construit sur mult permet de conclure (en convertissant les listes en multiset)
theory Scratch3
imports Main
"$ISABELLE_HOME/src/HOL/Library/Multiset_order"
begin
section{* A little theory on scalar products over multisets *}
definition scalar_prod :: "nat ⇒ 'a multiset ⇒ 'a multiset" (infix "⊗" 55)
where "n ⊗ S = Abs_multiset(λ m. (count S m) * n)"
lemma scalar_prod_zero [simp] : "0 ⊗ S = {#}"
unfolding scalar_prod_def plus_multiset_def
zero_multiset_def count_def map_fun_def o_def
by simp
lemma scalar_prod_Suc [simp] : "(Suc n) ⊗ S = S + (n ⊗ S)"
unfolding scalar_prod_def plus_multiset_def count_def map_fun_def o_def
by(simp_all add: multiset_def)
lemma scalar_prod_plus_distr [simp] : "(a ⊗ S) + (b ⊗ S) = ((a + b) ⊗ S)"
proof (induct "a" arbitrary: "b")
case 0 show ?case
by(simp)
next
case (Suc x) from Suc.hyps show ?case
by(simp add:Groups.semigroup_add_class.add.assoc)
qed
lemma scalar_prod_mult_distr [simp] : "a ⊗ (b ⊗ S) = (a * b) ⊗ S"
proof (induct "a" arbitrary: "b")
case 0 show ?case
by(simp)
next
case (Suc x) from Suc.hyps show ?case
by(simp add:Groups.semigroup_add_class.add.assoc)
qed
lemma count_scalar_distr [simp] : "count (b ⊗ S) x = (count S x) * b"
unfolding scalar_prod_def plus_multiset_def count_def map_fun_def o_def
apply(subst Multiset.multiset.Abs_multiset_inverse)
apply(simp_all add: multiset_def)
done
lemma multiset_of_replicate [simp] : "multiset_of (replicate s t) = s ⊗ {#t#}"
by(induct s, simp_all add: algebra_simps)
section{* Now comes the Application: A Termination Challenge Problem by Wolfgang Thumser*}
function (sequential) wot :: "nat list ⇒ nat list"
where "wot [] = []"
|"wot S = wot (butlast S @ replicate (last S - 1) (last S - 1))"
by pat_completeness auto
(* A validation of the definition ... *)
value "butlast [4,10::nat] @ replicate (last [10] - 1) (last [10] - 1)"
(* Now comes the challenge - the termination proof *)
termination
apply(relation "(S, S). (multiset_of S) #⊂# (multiset_of S)")
using Multiset_Order.wf_less_multiset[THEN Wellfounded.wf_inv_image,
of "multiset_of::nat list ⇒ nat multiset"]
apply(simp add: Relation.inv_image_def)
apply(auto intro: wf_mult1 wf_trancl simp: mult_def less_multiset_def)
apply(auto simp: mult1_def)
apply(rule r_into_trancl, simp)
apply(rule_tac x=v in exI,rule_tac x="{#}" in exI, simp)
apply(rule r_into_trancl, simp)
apply(rule_tac x="last va" in exI,rule_tac x="multiset_of (butlast va) + {#v#}" in exI, simp)
by (metis (full_types) add_eq_conv_ex append_butlast_last_id multiset_of_sorted_list_of_multiset sorted_list_of_multiset_singleton union_code)
end
Problèmes
Burkhart : problème avec "defs" dans Isabelle
Déclarer une constante, démontrer un théorème utilisant cette constante, puis définir la constante de façon à rendre le théorème faux (Ondřej Kunčar and Andrei Popescu, ITP 2015).
consts c::bool
typedef T = "{True, c}" by blast
lemma A: "c ⟷ (∀ (x::T) y. x = y)"
using Rep_T Rep_T_inject Abs_T_inject by (cases c) force+
defs c_bool_def: "c ≡ ¬(∀ (x::T) y. x=y)"
theorem F: False
using A c_bool_def by blast
theorem "Isabelle is consistent"
using F by blast
Previous meeting -- Next meeting