How to Make Ad Hoc Proof Automation Less Ad Hoc Georges Gonthier1 Beta Ziliani2 Aleks Nanevski3 Derek Dreyer2 1MicrosoftResearchCambridge 2MaxPlanckInstituteforSoftwareSystems(MPI-SWS) 3IMDEASoftwareInstitute,Madrid ICFP 2011, Tokyo Why proof automation at ICFP? Ad hoc polymorphism ≈ Overloading terms Ad hoc proof automation ≈ Overloading lemmas “How to make ad hoc polymorphism less ad hoc” Haskell type classes (Wadler & Blott ’89) “How to make ad hoc proof automation less ad hoc” Canonical structures: A generalization of type classes that’s already present in Coq G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc Motivating example from program verification Lemma noalias: If pointers x and x appear in disjoint heaps, they do not alias. 1 2 In formal syntax: noalias : ∀h : heap.∀x x : ptr.∀v : A .∀v : A . 1 2 1 1 2 2 def ( x (cid:55)→ v (cid:93) x (cid:55)→ v (cid:93) h ) → x != x 1 1 2 2 1 2 G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc Motivating example from program verification Lemma noalias: If pointers x and x appear in disjoint heaps, they do not alias. 1 2 In formal syntax: noalias : ∀h : heap.∀x x : ptr.∀v : A .∀v : A . 1 2 1 1 2 2 def ( x (cid:55)→ v (cid:93) x (cid:55)→ v (cid:93) h ) → x != x 1 1 2 2 1 2 singleton heaps G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc Motivating example from program verification Lemma noalias: If pointers x and x appear in disjoint heaps, they do not alias. 1 2 In formal syntax: noalias : ∀h : heap.∀x x : ptr.∀v : A .∀v : A . 1 2 1 1 2 2 def ( x (cid:55)→ v (cid:93) x (cid:55)→ v (cid:93) h ) → x != x 1 1 2 2 1 2 disjoint union (undefined if heaps overlap) G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc Motivating example from program verification Lemma noalias: If pointers x and x appear in disjoint heaps, they do not alias. 1 2 In formal syntax: noalias : ∀h : heap.∀x x : ptr.∀v : A .∀v : A . 1 2 1 1 2 2 def ( x (cid:55)→ v (cid:93) x (cid:55)→ v (cid:93) h ) → x != x 1 1 2 2 1 2 test for definedness/disjointness G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc Motivating example from program verification Lemma noalias: If pointers x and x appear in disjoint heaps, they do not alias. 1 2 In formal syntax: noalias : ∀h : heap.∀x x : ptr.∀v : A .∀v : A . 1 2 1 1 2 2 def ( x (cid:55)→ v (cid:93) x (cid:55)→ v (cid:93) h ) → x != x 1 1 2 2 1 2 no alias G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc Using noalias requires a lot of “glue proof” noalias : ∀h x x v v . 1 2 1 2 def (x (cid:55)→ v (cid:93) x (cid:55)→ v (cid:93) h) → x != x 1 1 2 2 1 2 D : def (h (cid:93) (y (cid:55)→ w (cid:93) y (cid:55)→ w ) (cid:93) (h (cid:93) y (cid:55)→ w )) 1 1 1 2 2 2 3 3 (y != y ) && (y != y ) && (y != y ) 1 2 2 3 3 1 G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc Using noalias requires a lot of “glue proof” noalias : ∀h x x v v . 1 2 1 2 def (x (cid:55)→ v (cid:93) x (cid:55)→ v (cid:93) h) → x != x 1 1 2 2 1 2 D : def (h (cid:93) (y (cid:55)→ w (cid:93) y (cid:55)→ w ) (cid:93) (h (cid:93) y (cid:55)→ w )) 1 1 1 2 2 2 3 3 (y != y ) && (y != y ) && (y != y ) 1 2 2 3 3 1 G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc Using noalias requires a lot of “glue proof” noalias : ∀h x x v v . 1 2 1 2 def (x (cid:55)→ v (cid:93) x (cid:55)→ v (cid:93) h) → x != x 1 1 2 2 1 2 D : def (h (cid:93) (y (cid:55)→ w (cid:93) y (cid:55)→ w ) (cid:93) (h (cid:93) y (cid:55)→ w )) 1 1 1 2 2 2 3 3 (y != y ) && (y != y ) && (y != y ) 1 2 2 3 3 1 G.Gonthier,B.Ziliani,A.Nanevski,D.Dreyer HowtoMakeAdHocProofAutomationLessAdHoc