LRI
Équipe MODHEL
Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on September 23 2015

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