-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathsection7.v
39 lines (29 loc) · 1.35 KB
/
section7.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
(******************************************************************************)
(* Solutions of exercises : Appendix *)
(******************************************************************************)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import choice fintype tuple finset.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
(******************************************************************************)
(* Exercise 7.0.3 *)
(******************************************************************************)
Search _ "_ * _".
Print muln.
Print muln_rec.
Search _ "_ ==> _".
Print implb.
Search (_ ==> true).
Search _ (_ && _ = _ && _).
(******************************************************************************)
(* Exercise 7.0.4 *)
(******************************************************************************)
(* According to the name of the operator and to the table of suffixes *)
(*it should be mulnC *)
Search (_ * _ = _ * _).
(* The above command does not work since commutativity for muln is *)
(*stated using the predicate on binary operations *)
Search _ commutative muln.
Check orbCA.
Print left_commutative.