Library UniMath.Algebra.Universal.Examples.Bool
Example on booleans.
Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021Require Import UniMath.MoreFoundations.Notations.
Require Import UniMath.MoreFoundations.Bool.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.Combinatorics.MoreLists.
Require Import UniMath.Algebra.Universal.Algebras.
Require Import UniMath.Algebra.Universal.VTerms.
Local Open Scope stn.
Definition bool_signature := make_signature_simple_single_sorted [0; 0; 1; 2; 2; 2].
Definition bool_algebra := make_algebra_simple_single_sorted bool_signature boolset
[(
λ _, false ;
λ _, true ;
λ x, negb (pr1 x) ;
λ x, andb (pr1 x) (pr12 x) ;
λ x, orb (pr1 x) (pr12 x) ;
λ x, implb (pr1 x) (pr12 x)
)].
The type of ground terms.
Constructors for ground terms.
Definition bot : T := build_gterm_curried (●0 : names bool_signature).
Definition top : T := build_gterm_curried (●1 : names bool_signature).
Definition neg : T → T := build_gterm_curried (●2 : names bool_signature).
Definition conj : T → T → T := build_gterm_curried (●3 : names bool_signature).
Definition disj : T → T → T := build_gterm_curried (●4 : names bool_signature).
Definition impl : T → T → T := build_gterm_curried (●5 : names bool_signature).
End GTerm.
Type for boolean (open) terms.
Constructors for terms.
Definition bot : T := build_term_curried (●0 : names bool_signature).
Definition top : T := build_term_curried (●1 : names bool_signature).
Definition neg : T → T := build_term_curried (●2 : names bool_signature).
Definition conj : T → T → T := build_term_curried (●3 : names bool_signature).
Definition disj : T → T → T := build_term_curried (●4 : names bool_signature).
Definition impl : T → T → T := build_term_curried (●5 : names bool_signature).
Interpretation of propositional formulae.
Definition interp (α: assignment bool_algebra bool_varspec) (t: T) : bool :=
fromterm (ops bool_algebra) α tt t.
Computations and interactive proofs.
Module Tests.
Definition x : T := varterm (0: bool_varspec).
Definition y : T := varterm (1: bool_varspec).
Definition z : T := varterm (2: bool_varspec).
Example: evaluation of true & false
A simple evaluation function for variables:
assign true to x and y (the 0th and 1st variable) and false otherwise.
Example: evaluation of x ∧ (¬ y ∧ z)
Example: evaluation of x ∧ (z → ¬ y)
Dummett tautology
Local Lemma Dummett : ∏ i, interp i (disj (impl x y) (impl y x)) = true.
Proof.
intro i. lazy.
induction (i 0); induction (i 1); apply idpath.
Qed.
x ∨ ¬ (y ∧ z → x)
Local Lemma not_tautology : ∑ i, interp i (disj x (neg (impl (conj y z) x))) = false.
Proof.
use tpair.
- exact (λ n, match n with _ ⇒ false end).
- lazy.
apply idpath.
Qed.
Further tests.