(Joint Center)Library tutorial

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

Section HilbertSaxiom.

Variables A B C : Prop.

Lemma HilbertS : (ABC) → (AB) → AC.

Hypotheses (hAiBiC : ABC) (hAiB : AB) (hA : A).

Lemma HilbertS2 : C.

Check (hAiB hA).

Lemma HilbertS3 : C.

Lemma HilbertS4 : C.

Lemma HilbertS5 : C.

Lemma HilbertS6 : C.

End HilbertSaxiom.

Section Symmetric_Conjunction_Disjunction.

Print bool.

Lemma andb_sym : A B : bool, A && BB && A.

Lemma andb_sym2 : A B : bool, A && BB && A.

Lemma andb_sym3 : A B : bool, A && BB && A.

Variables (C D : Prop) (hC : C) (hD : D).
Check (and C D).
Print and.
Check conj.
Check (conj hC hD).

Lemma and_sym : A B : Prop, ABBA.

Print or.

Check or_introl.

Lemma or_sym : A B : Prop, ABBA.

Lemma or_sym2 : A B : bool, ABBA.

End Symmetric_Conjunction_Disjunction.

Section R_sym_trans.

Variables (D : Type) (R : DDProp).

Hypothesis R_sym : x y, R x yR y x.

Hypothesis R_trans : x y z, R x yR y zR x z.

Lemma refl_if : x : D, ( y, R x y) → R x x.

End R_sym_trans.

Section Smullyan_drinker.

Variables (D : Type) (P : DProp).
Hypotheses (d : D) (EM : A, A ∨ ¬A).

Lemma drinker : x, P x y, P y.

End Smullyan_drinker.

Section Equality.

Variable f : natnat.
Hypothesis f00 : f 0 = 0.

Lemma fkk : k, k = 0 → f k = k.

Lemma fkk2 : k, k = 0 → f k = k.

Variable f10 : f 1 = f 0.

Lemma ff10 : f (f 1) = 0.

Variables (D : eqType) (x y : D).

Lemma eq_prop_bool : x = yx == y.

Lemma eq_bool_prop : x == yx = y.

End Equality.

Section Using_Definition.

Variable U : Type.

Definition set := UProp.

Definition subset (A B : set) := x, A xB x.

Definition transitive (T : Type) (R : TTProp) :=
  x y z, R x yR y zR x z.

Lemma subset_trans : transitive set subset.

Lemma subset_trans2 : transitive set subset.

End Using_Definition.

Section Basic_ssrnat.

Lemma three : S (S (S O)) = 3 ∧ 3 = 0.+1.+1.+1.

Lemma concrete_plus : plus 16 64 = 80.
(*simpl.*)
Lemma concrete_addn : 16 + 64 = 80.
(*simpl.*)
Lemma concrete_le : le 1 3.

Lemma concrete_big_le : le 16 64.

Lemma concrete_big_leq : 0 ≤ 51.

Lemma semi_concrete_leq : n m, nm → 51 + n ≤ 51 + m.

Lemma concrete_arith : (50 < 100) && (3 + 4 < 3 × 4 ≤ 17 - 2).

Lemma plus_com : m1 n1, n1 + m1 = m1 + n1.

End Basic_ssrnat.

Section Euclidean_division.

Set Implicit Arguments.

Definition edivn_rec d := fix loop (m q : nat) {struct m} :=
  if m - d is m'.+1 then loop m' q.+1 else (q, m).

Definition edivn m d := if d is d'.+1 then edivn_rec d' m 0 else (0, m).

CoInductive edivn_spec (m d : nat) : nat × natType :=
  EdivnSpec q r of m = q × d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r).

Lemma edivnP : m d, edivn_spec m d (edivn m d).

Lemma edivn_eq : d q r, r < dedivn (q × d + r) d = (q, r).

CoInductive edivn_spec_right : natnatnat × natType :=
  EdivnSpec_right m d q r of m = q × d + r & (d > 0) ==> (r < d) :
  edivn_spec_right m d (q, r).

CoInductive edivn_spec_left (m d : nat)(qr : nat × nat) : Type :=
EdivnSpec_left of m = (fst qr) × d + (snd qr) & (d > 0) ==> (snd qr < d) :
   edivn_spec_left m d qr.

Lemma edivnP_left : m d, edivn_spec_left m d (edivn m d).

Lemma edivnP_right : m d, edivn_spec_right m d (edivn m d).

Lemma edivn_eq_right : d q r, r < dedivn (q × d + r) d = (q, r).

Lemma edivn_eq_left : d q r, r < dedivn (q × d + r) d = (q, r).

End Euclidean_division.