A macro to prove congruence rules for quantified formulae and their associated witnesses
The
Usage:
(include-book "coi/quantification/quantified-congruence" :dir :system) ;; Given a predicate that satisfies some congruence (defcong pred-equiv equal (pred a x y) 2) ;; A quantified formula involving pred introduced using ;; defun-sk with the :strengthen t option. (defun-sk quantified-pred (v z) (forall (a) (pred a v z)) :strengthen t) ;; We prove congruence rules relative to 'v' (quant::congruence quantified-pred (v z) (forall (a) (pred a v z)) :congruences ((v pred-equiv))) ;; The following lemmas now follow directly .. (defthmd witness-congruence (implies (pred-equiv v1 v2) (equal (quantified-pred-witness v1 z) (quantified-pred-witness v2 z)))) (defthmd quantified-congruence (implies (pred-equiv v1 v2) (equal (quantified-pred v1 z) (quantified-pred v2 z))))