Boolean reflection via type classes

Description

Boolean reflection is a formalization technique that represents decidable predicates with their decision procedures and where truth values become booleans. Reflection occurs in the small scale: since conjectures are stated using programs their symbolic execution provides a valuable form of automation. In this approach the user faces the " syntactic " (bool) representation of the conjecture and is given tactic-level tools to switch to the " semantic " one (Prop) and back. The SSReflect proof language [1] provides the view mechanism to switch from the computational realm of bool to the semantic one of Prop. To minimize the syntactic noise due to view application SSReflect accepts views as annotations of most linguistic constructs. Still a user needs to mention the view name explicitly, even when there is only one view to be applied. We propose a type-class [2] based machinery to attach canonical views to predicates and connectives to relief the Coq user from some of the bookkeeping required by the boolean reflection formalization technique. Let's take a very simple example. Here the is_true constant is used to state the truth of a boolean predicates. Being declared as a coercion is automatically inserted by Coq around any boolean value occurring in a context expecting a Prop. The support lemmas andP and orP are views linking the boolean connec-tives && and || to their meaning in Prop. The reflect predicate simply states that its first argument, in Prop, holds if and only its second argument, in bool, is equal to true. Definition is_true b := b = true. Coercion is_true : bool >-> Sortclass. (* Prop *) Lemma andP b1 b2 : reflect (b1 /\ b2) (b1 && b2). Lemma orP b1 b2 : reflect (b1 \/ b2) (b1 || b2). Lemma example_bool a b : ((a && b) || a)-> a Proof. by move=> /orP[ /andP[ Ha Hb ] | Ha ]; assumption. Qed. Lemma example_prop a b : ((a /\ b) \/ a)-> a Proof. by move=> [ [ Ha Hb ] | Ha ]; assumption. Qed. The example_bool proof 1 applies the two views in order to de-structure the assumption. The second proof needs no such bookkeeping, since the conjecture is already stated in Prop. We propose a declarative way of associating canonical views to connectives and predicates and a generic view name xP to select the view fitting the current 1 A much simples proof would be to enumerate truth values as in " by case a; case b ". For the sake of clarity we picked an oversimple example.

Abstract

International audience

Additional details