# Differences

This shows you the differences between two versions of the page.

 sav08:theorems_as_abstract_data_types [2008/05/28 05:32]vkuncak sav08:theorems_as_abstract_data_types [2008/05/28 06:03] (current)vkuncak Both sides previous revision Previous revision 2008/05/28 06:03 vkuncak 2008/05/28 05:32 vkuncak 2008/05/28 05:29 vkuncak created 2008/05/28 06:03 vkuncak 2008/05/28 05:32 vkuncak 2008/05/28 05:29 vkuncak created Line 16: Line 16: Soundness of the approach: if a value of type '​theorem'​ is computed, we know there exists an expression formed from ADT operations. ​ This means that there is a proof tree, so the value is a theorem. Soundness of the approach: if a value of type '​theorem'​ is computed, we know there exists an expression formed from ADT operations. ​ This means that there is a proof tree, so the value is a theorem. + + ===== Example Operations of Theorem ADT ===== + + Often proof manipulating or even ADT functions are partial. ​ We can express this using algebraic data types with alterbatives (e.g. option types), or using exceptions. ​ These features, as implemented in ML do not compromise type safety. ​ We illustrate this using propositional logic. + + abstype theorem + groundT : formula -> theorem option // returns a theorem if given formula is ground and evaluates to true + inspect : theorem -> formula // return formula for theorem so we can decide how to prove it + cases : theorem -> theorem -> formula -> variable -> theorem option + andI : theorem -> theorem -> theorem ​ + andE1 : theorem -> theorem option + + Here 'cases t1 t2 f x' will compute f[x:=true] and check that it is identical to t1, then compute f[x:=false] and check it is identical to t2.  If both tests succeed, it will return f as a theorem. + + The '​andI'​ (and introduction) function takes two theorems and computes their conjunction,​ which is also a theorem. + + The '​andE1'​ (first and-elimination) takes a theorem, checks whether it has the form 't1 & t2'​. ​ If so, it returns t1. + + Using such ADT we can build a prover that is guaranteed to either produce correct result or fail (it will never produce a formula that is a non-theorem). + + let rec prove (f : form) : theorem option = + if (isGround f) then (groundT f) + else (let v = getOneFreeVar f in + match (prove (subst [(v,True)] f), prove (subst [(v,False)] f)) with + | (Some t1, Some t2) -> cases t1 t2 f v + | _ -> None) + + It can be tedious to propagate possible errors. ​ This is why exceptions are so useful. + + + ===== Tactic and Tacticals ===== + + Tactics accept formulas and try to produce the theorem containing this formula. + + Tatics can often be combined into bigger tatics using higher-order functions called tacticals (for example, alternative,​ sequencing, repetition).