Boolean reflection via type classes

Benjamin Grégoire 1 Enrico Tassi 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Type de document :
Communication dans un congrès
Coq Workshop, Aug 2016, Nancy, France. 2016
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01410530
Contributeur : Enrico Tassi <>
Soumis le : mardi 6 décembre 2016 - 16:48:25
Dernière modification le : jeudi 11 janvier 2018 - 16:36:44
Document(s) archivé(s) le : mardi 21 mars 2017 - 09:17:59

Fichier

autoview.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Copyright (Tous droits réservés)

Identifiants

  • HAL Id : hal-01410530, version 1

Collections

Citation

Benjamin Grégoire, Enrico Tassi. Boolean reflection via type classes. Coq Workshop, Aug 2016, Nancy, France. 2016. 〈hal-01410530〉

Partager

Métriques

Consultations de la notice

191

Téléchargements de fichiers

80