		Search-engine friendly clone of the ACL2 documentation.

Defun-sk

Congruence

A macro to prove congruence rules for quantified formulae and their associated witnesses

The quant::congruence macro can be used to prove ACL2::congruence rules for quantified formulae and their associated witnesses introduced using defun-sk. Note: this macro only works for formula that are introduced with the :strengthen t keyword.

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))))