class: center, middle # Towards conditional laws # in Hipster **Irene Lobo Valbuena** @ Chalmers University of Technology On-going MSc thesis Supervisor: **Moa Johansson** *2^nd Workshop on Automated Inductive Theorem-proving*; March 2015 .footnote[ {created with [remark](http://remarkjs.com/)} ] --- # Goal Generation and treatment of conditional lemmas within a scope of assumptions. .center[] ??? Discover missing lemmas for and via inductive proofs => added to background theory => allowing for the use of automated tactics for more (inductive) proofs Equational limitation => extend Hipster with support for conditional lemmas Eg: required when reasoning about sorting algorithms, treating different branches of a proof along with their specific conditions --- # Why conditional lemmas Equational lemmas: useful properties and insight. Reasoning within a specific frame or context => restriction over the structure of objects involved: - during a (stuck) proof attempt: branching on cases - invariants: preservation of (data)type invariants - algorithm/method correction Enable automated proofs of later lemmas => enable discovering more lemmas! ??? Equational lemmas: mathematical structure Already existing built-in automated tactics of Isabelle may fail to provide a proof at that stage; theory exploration might reveal interesting lemmas conditioned by the current context that were missing. Gradual refining towards bigger theorems. --- .center[] Operation properties ```isabelle xs ≠ [] ⟹ head (xs @ ys) = head xs ``` Algorithm correctness ```isabelle sorted ts ⟹ sorted (insert t ts) ``` .footnote[ {img source - http://paulscottinfo.ipage.com/fractals/} ] ??? All under the umbrella of induction (inductive invariants) Induction: repetition: recursion, iteration. `sorted (isort ts)` requires inductive cond. lemma --- ## Extensions required - Postulate conditional lemmas: how? * too strong, too weak * bound by constructor structure * combinatorial problem => Simplify: have a given condition * extract from working context * user-specified - Automated induction tactic extension * conditionals requiring induction ??? How to speculate interesting side-conditions? Current state + first step: a given single predicate as a condition (extract from working context (stuck proof) or specified by a user) conditionals not proven yet by Hipster's tactic prune away trivial proofs --- name: ingredients # A tactic (not only) for conditionals Automation ingredients: - Induction - Simplification - Metis FO prover ??? --- template: ingredients But... * What to induct on? * Simplifier rules? * Facts for Metis? --- name: first-stop ## First stop: Recursion induction Conditionals: * construction => structural induction * recursive condition/property => recursion induction Isolate structural (sub)units not represented in the implementational construction. ??? In relation to the way in which it is constructed --- template: first-stop ```isabelle ?P Nil ⟹ (⋀a List. ?P List ⟹ ?P (Cons a List)) ⟹ ?P ?List ``` ```isabelle (⋀ts. ?P Z ts) ⟹ (⋀v. ?P (S v) Nil) ⟹ (⋀n t ts. ?P n ts ⟹ ?P (S n) (Cons t ts)) ⟹ ?P ?a0.0 ?a1.0 ``` ```isabelle ?P Nil ⟹ (⋀uu_. ?P (Cons uu_ Nil)) ⟹ (⋀r t ts. ?P (Cons t ts) ⟹ ?P (Cons r (Cons t ts))) ⟹ ?P ?a0.0 ``` ??? Isabelle: induction schemata derived from recursive functions => good candidates to consider in Hipster's tactics. Exploit current system poss's --- name: take-drop ## [1] take & drop ```isabelle (⋀ts. ?P Z ts) ⟹ (⋀v. ?P (S v) Nil) ⟹ (⋀n t ts. ?P n ts ⟹ ?P (S n) (Cons t ts)) ⟹ ?P ?a0.0 ?a1.0 ``` ```isabelle lemma dropTake : "ts = app (take n ts) (drop n ts)" apply(induction ts) sledgehammer apply (metis drop.simps(1) drop.simps(2) take.simps(1) take.simps(2) Nat.exhaust app.simps(1)) sledgehammer ``` => Time-out --- template: take-drop ```isabelle lemma dropTake : "ts = app (take n ts) (drop n ts)" apply(induction ts rule: take.induct) by simp_all ``` ??? Reduced metis steps Really benefits from induction scheme `drop.induct` --- template: take-drop ```isabelle lemma dropTake : "ts = app (take n ts) (drop n ts)" by hipster_induct_schemes ``` ??? (new possible automated proofs) Automate choice: rule + var(s) --- name: sorting ## [2] sorting ```isabelle ?P Nil ⟹ (⋀uu_. ?P (Cons uu_ Nil)) ⟹ (⋀r t ts. ?P (Cons t ts) ⟹ ?P (Cons r (Cons t ts))) ⟹ ?P ?a0.0 ``` ```isabelle lemma insSortInvar : "sorted ts ⟹ sorted (insert t ts)" apply(induction ts rule: sorted.induct) apply(simp_all) by metis lemma isortSorts : "sorted (isort ts)" by (hipster_induct_simp_metis insSortInvar) ``` --- name: sorting ## [2] sorting ```isabelle ?P Nil ⟹ (⋀uu_. ?P (Cons uu_ Nil)) ⟹ (⋀r t ts. ?P (Cons t ts) ⟹ ?P (Cons r (Cons t ts))) ⟹ ?P ?a0.0 ``` ```isabelle lemma insSortInvar : "sorted ts ⟹ sorted (insert t ts)" by hipster_induct_schemes lemma isortSorts : "sorted (isort ts)" by (hipster_induct_simp_metis insSortInvar) ``` --- template: sorting ```isabelle lemma isortIds : "sorted ts ⟹ isort ts = ts" by hipster_induct_schemes lemma isortFixes : "isort (isort ts) = isort ts" by (metis isortSorts isortIds) lemma isortIdsP : "sorted ts ⟹ sorted (isort ts)" by (metis isortSorts) ``` ??? (new possible automated proofs) timeouts when no rules... - simplify other proofs - easier to prune trivialities (`isortIdsP`) --- # Overall **Advance towards automation** More refinement needed - Side-condition vs conclusion driven induction? - Heuristics: variables to favour - Simpset? **Full automation is hard** - Single induction per proof attempt - need for more: bound? - Common need for simultaneous induction ```isabelle lemma appZips: "len a = len b ⟹ app (zip a b) (zip c d) = zip (app a c) (app b d)" apply(induction a b rule: zip.induct) apply(simp_all) by (metis app.simps len.simps List.exhaust Nat.distinct) ``` ??? Less stuff passed on to metis, less manual More to look at - lemma subsumption - heuristic to define an order of proving - refine lemmas passed on to tactics (`simp`, `metis`, etc.): execution time * looping in simp may prevent finding an already possible proof => size of cond's vs conclusions? automate criterion for inclusion in simp or not... - mutual inductions? reasonable bound to number of inductions? --- # Next: theory exploration ## Underlying tools - QuickSpeck (via HipSec) * strong equational support * more to come up! ## First focus - User-supplied conditions - Condition extraction from context .footnote[ {current state: [induct-schemes-tac@IsaHipster]( https://github.com/moajohansson/IsaHipster/tree/induct-schemes-tac/)} ] ??? Conditional lemma provided/suggested by user; try to prove: already ok predicate provided by the user: limited exploration currently; suggestions automatically proven or *left as an exercise* --- class: center, middle # Q ⟹ ?'a --- ## [0] Structure - construction vs operations ```isabelle datatype 'a list = Nil | Cons'a "'a list" datatype 'a openL = Stop | Sing 'a | FrontBack 'a "'a openL" 'a ``` ```isabelle fun lastD :: "'a openL ⇒ 'a" where "lastD (Sing t) = t" | "lastD (FrontBack x ts y) = y" fun headD :: "'a openL ⇒ 'a" where "headD (Sing t) = t" | "headD (FrontBack x ts y) = x" ``` ```isabelle fun head :: "'a List ⇒ 'a" where "head (Cons t _) = t" fun last :: "'a List ⇒ 'a" where "last (Cons t Nil) = t" | "last (Cons _ ts) = last ts" ``` ??? (a simple) Motivation example for considering recursion-induction schemata. --- name: front-back ## [0] Structure - construction vs operations ```isabelle fun revD :: "'a openL ⇒ 'a openL" where "revD Stop = Stop" | "revD (Sing x) = Sing x" | "revD (FrontBack t xs r) = FrontBack r (revD xs) t" fun rev :: "'a List ⇒ 'a List" where "rev Nil = Nil" | "rev (Cons r ts) = app (rev ts) (Cons r Nil)" ``` Using sledgehammer... ```isabelle lemma lastElemIsLast: "last (app ts (Cons t Nil)) = t" apply(induction ts) apply(simp_all) sledgehammer by (metis List.exhaust last.simps(2) app.simps) ``` --- template: front-back Recursion induction scheme... ```isabelle lemma lastElemIsLastR: "last (app ts (Cons t Nil)) = t" apply(induction ts rule: last.induct) by simp_all ``` --- template: front-back Automation! ```isabelle lemma lastElemIsLastR: "last (app ts (Cons t Nil)) = t" by (hipster_induct_schemes) ``` --- name: first-last ## [0] Structure - construction vs operations ```isabelle fun revD :: "'a openL ⇒ 'a openL" where "revD Stop = Stop" | "revD (Sing x) = Sing x" | "revD (FrontBack t xs r) = FrontBack r (revD xs) t" fun rev :: "'a List ⇒ 'a List" where "rev Nil = Nil" | "rev (Cons r ts) = app (rev ts) (Cons r Nil)" ``` Requires an auxiliary lemma (theory exploration!) ```isabelle lemma firstLast: "ts ≠ Nil ⟹ head ts = last (rev ts)" by (metis rev.simps(2) head.cases head.simps lastElemIsLast) ``` ```isabelle lemma firstLastD: "ts ≠ Stop ⟹ headD ts = lastD (revD ts)" by (metis DubL.exhaust headD.simps lastD.simps revD.simps) ``` ??? Both reproducible with: by hipster_induct_simp_metis And auxiliary lemma: implementation structure requirement => recursion induction! --- ## [0] Structure - construction vs operations * `List.induct` ```isabelle ?P Nil ⟹ (⋀a List. ?P List ⟹ ?P (Cons a List)) ⟹ ?P ?List ``` * `last.induct` ```isabelle (⋀t. ?P (Cons t Nil)) ⟹ (⋀uu_ v va. ?P (Cons v va) ⟹ ?P (Cons uu_ (Cons v va))) ⟹ ?P Nil ⟹ ?P ?a0.0 ``` * `openL.induct` ```isabelle ?P Stop ⟹ (⋀a. ?P (Sing a)) ⟹ (⋀a1 openL a2. ?P openL ⟹ ?P (FrontBack a1 openL a2)) ⟹ ?P ?openL ``` * `lastD.induct` ```isabelle (⋀t. ?P (Sing t)) ⟹ (⋀x ts y. ?P (FrontBack x ts y)) ⟹ ?P Stop ⟹ ?P ?a0.0 ``` ??? `openL.induct` == `lastD.induct` Not so for `List`: new pattern/sub-structures needing consideration --- # Sort functions ```isabelle fun sorted :: "Nat List ⇒ bool" where "sorted Nil = True" | "sorted (Cons _ Nil) = True" | "sorted (Cons r (Cons t ts)) = (leq r t ∧ sorted (Cons t ts))" fun insert :: "Nat ⇒ Nat List ⇒ Nat List" where "insert r Nil = Cons r Nil" | "insert r (Cons t ts) = (if leq r t then Cons r (Cons t ts) else (Cons t (insert r ts)))" fun isort :: "Nat List ⇒ Nat List" where "isort Nil = Nil" | "isort (Cons t ts) = insert t (isort ts)" ```