LogicIntro19
LogicIntro: Introduction to logic, propositions and proofs
Set Warnings "-notation-overridden,-parsing".
From Coq Require Import ssreflect ssrbool ssrfun.
From Coq Require Import ssreflect ssrbool ssrfun.
In previous chapters, we have seen many examples of factual
claims (propositions) and ways of presenting evidence of their
truth (proofs). In particular, we have worked extensively with
equality propositions of the form e1 = e2, with
implications (P → Q), and with quantified propositions (∀
x, P). In this chapter, we will see how Coq can be used to carry
out other familiar forms of logical reasoning.
Before diving into details, let's talk a bit about the status of
mathematical statements in Coq. Recall that Coq is a typed
language, which means that every sensible expression in its world
has an associated type. Logical claims are no exception: any
statement we might try to prove in Coq has a type, namely Prop,
the type of propositions. We can see this with the Check
command:
Check 3 = 3.
(* ===> Prop *)
Check ∀n m : nat, n + m = m + n.
(* ===> Prop *)
(* ===> Prop *)
Check ∀n m : nat, n + m = m + n.
(* ===> Prop *)
Note that all syntactically well-formed propositions have type
Prop in Coq, regardless of whether they are true or not.
Simply being a proposition is one thing; being provable is
something else!
Check ∀n : nat, n = 2.
(* ===> Prop *)
Check 3 = 4.
(* ===> Prop *)
(* ===> Prop *)
Check 3 = 4.
(* ===> Prop *)
Indeed, propositions don't just have types: they are first-class
objects that can be manipulated in the same ways as the other
entities in Coq's world. So far, we've seen one primary place
that propositions can appear: in Theorem (and Lemma and
Example) declarations.
Theorem plus_2_2_is_4 :
2 + 2 = 4.
Proof. reflexivity. Qed.
2 + 2 = 4.
Proof. reflexivity. Qed.
But propositions can be used in many other ways. For example, we
can give a name to a proposition using a Definition, just as we
have given names to expressions of other sorts.
Definition plus_fact : Prop := 2 + 2 = 4.
Check plus_fact.
(* ===> plus_fact : Prop *)
Check plus_fact.
(* ===> plus_fact : Prop *)
We can later use this name in any situation where a proposition is
expected — for example, as the claim in a Theorem declaration.
Theorem plus_fact_is_true :
plus_fact.
Proof. reflexivity. Qed.
plus_fact.
Proof. reflexivity. Qed.
We can also write parameterized propositions — that is,
functions that take arguments of some type and return a
proposition.
For instance, the following function takes a number
and returns a proposition asserting that this number is equal to
three:
Definition is_three (n : nat) : Prop :=
n = 3.
Check is_three.
(* ===> nat -> Prop *)
n = 3.
Check is_three.
(* ===> nat -> Prop *)
In Coq, functions that return propositions are said to define
properties of their arguments.
For instance, here's a (polymorphic) property defining the
familiar notion of an injective function.
Definition injective {A B} (f : A → B) :=
∀x y : A, f x = f y → x = y.
Lemma succ_inj : injective S.
Proof.
move⇒ n m. by case.
Qed.
∀x y : A, f x = f y → x = y.
Lemma succ_inj : injective S.
Proof.
move⇒ n m. by case.
Qed.
The equality operator = is also a function that returns a
Prop.
The expression n = m is syntactic sugar for eq n m, defined
using Coq's Notation mechanism. Because eq can be used with
elements of any type, it is also polymorphic:
Check @eq.
(* ===> forall A : Type, A -> A -> Prop *)
(* ===> forall A : Type, A -> A -> Prop *)
(Notice that we wrote @eq instead of eq: The type
argument A to eq is declared as implicit, so we need to turn
off implicit arguments to see the full type of eq.)
This is a good opportunity to return to our slogan from the poster, recall ...
... proofs are programs and programs are proofs!
Programming and proving in Coq are two sides of the same coin.
Proving manipulates evidence, much as programs manipulate data.
Question: If evidence is data, what are propositions themselves?
Answer: They are types!
Suppose we introduce an alternative pronunciation of ":". (In statements of theorems, not as a ssreflect tactical of course).
Instead of "has type," we can say "is a proof of" ...
This pun between types and propositions — between : as "has type"
and : as "is a proof of" or "is evidence for" — is called the
Curry-Howard correspondence. It proposes a deep connection
between the world of logic and the world of computation:
Question: How do you define the meaning of a proposition?
The meaning of a proposition is given by rules and definitions
that say how to construct evidence for the truth of the
proposition from other evidence.
"Algorithms are the computational content of proofs." —Robert Harper
propositions ~ types proofs ~ data valuesMany useful insights follow from this connection.
Understanding Prop and logic in Coq
- begins with the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic proposed in the late 1920's and early 1930's
- more recently, continues with Martin-Löf ...
- Typically, rules are defined inductively, just like any other
datatype.
- Sometimes a proposition is declared to be true without substantiating evidence. Such propositions are called axioms.
Natural deduction
- A formal calculus which makes this process of constructing evidence explicit is called natural deduction.
- It was first proposed by Gerhard Gentzen in the 1930's.
- It gives the meaning of each connective by its introduction and destruction (elimination) rules.
- Those of you who have done a recent version of GLoIn, have seen a Fitch-style variant of ND.
- From Coq's point of view, introduction rules say how to prove a proposition involving a given connective.
- Elimination rules say how to use or apply hypotheses (or earlier lemmas) using this connective in new proofs.
- What we are doing with Coq is assisted proof search.
- We start with the ultimate result we want to obtain, the sentence we want to hold true.
- That is, we begin at the bottom of proof tree to be built and try find a way bottom-up to its branches: premises living in the context we have.
Logical Connectives
Conjunction
Check and.
(* ===>
and: Prop -> Prop -> Prop *)
Print and.
(* ===>
Inductive and (A B : Prop) : Prop := conj : A -> B -> A /\ B *)
(* ===>
and: Prop -> Prop -> Prop *)
Print and.
(* ===>
Inductive and (A B : Prop) : Prop := conj : A -> B -> A /\ B *)
Notice the similarity with the definition of the prod type,
given in chapter Poly; the only difference is that prod takes
Type arguments, whereas and takes Prop arguments.
Print prod.
(* ===>
Inductive prod (A B : Type) : Type :=
| pair : A -> B -> A * B. *)
(* ===>
Inductive prod (A B : Type) : Type :=
| pair : A -> B -> A * B. *)
Conjunction: proving it
| Gamma ⊢ A Gamma ⊢ B | (/\ I) |
| Gamma ⊢ A ∧ B |
Example and_example : 3 + 4 = 7 ∧ 2 * 2 = 4.
Proof.
split.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
Proof.
split.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
In fact, for a type with a single constructor taking two arguments, split is just a wrapper for applying this constructor; in this case, apply conj.
Example and_example' : 3 + 4 = 7 ∧ 2 * 2 = 4.
Proof.
apply conj.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
Proof.
apply conj.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
In ssreflect, our good old friend by [] is more than enough.
Example and_example'' : 3 + 4 = 7 ∧ 2 * 2 = 4.
Proof.
by [].
Qed.
Proof.
by [].
Qed.
Lemma and_intro : ∀A B : Prop, A → B → A ∧ B.
Proof.
by [].
(*
intros A B HA HB. split.
- apply HA.
- apply HB.*)
Qed.
Proof.
by [].
(*
intros A B HA HB. split.
- apply HA.
- apply HB.*)
Qed.
Since applying a theorem with hypotheses to some goal has the
effect of generating as many subgoals as there are hypotheses for
that theorem, we can apply and_intro to achieve the same effect
as split.
Example and_example''' : 3 + 4 = 7 ∧ 2 * 2 = 4.
Proof.
apply and_intro.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
Proof.
apply and_intro.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
Example and_exercise :
∀n m : nat, n + m = 0 → n = 0 ∧ m = 0.
Proof.
(* FILL IN HERE *) Admitted.
☐
∀n m : nat, n + m = 0 → n = 0 ∧ m = 0.
Proof.
(* FILL IN HERE *) Admitted.
Conjunction: using it
| Gamma ⊢ A ∧ B | (/\ E_l) |
| Gamma ⊢ A |
| Gamma ⊢ A ∧ B | (/\ E_r) |
| Gamma ⊢ B |
Lemma and_example2 :
∀n m : nat, n = 0 ∧ m = 0 → n + m = 0.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ?.
case ⇒ [Hn Hm].
rewrite Hn Hm.
by [].
Qed.
∀n m : nat, n = 0 ∧ m = 0 → n + m = 0.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ?.
case ⇒ [Hn Hm].
rewrite Hn Hm.
by [].
Qed.
As usual, we can also destruct H right when we introduce it,
instead of introducing and then destructing it:
Lemma and_example2' :
∀n m : nat, n = 0 ∧ m = 0 → n + m = 0.
Proof.
move ⇒ ? ? [Hn Hm].
rewrite Hn Hm.
by [].
(* OR: intros n m Hn Hm.
rewrite Hn. rewrite Hm.
reflexivity.*)
Qed.
∀n m : nat, n = 0 ∧ m = 0 → n + m = 0.
Proof.
move ⇒ ? ? [Hn Hm].
rewrite Hn Hm.
by [].
(* OR: intros n m Hn Hm.
rewrite Hn. rewrite Hm.
reflexivity.*)
Qed.
You may wonder why we bothered packing the two hypotheses n = 0
and m = 0 into a single conjunction, since we could have also
stated the theorem with two separate premises:
Lemma and_example2'' :
∀n m : nat, n = 0 → m = 0 → n + m = 0.
Proof.
intros n m Hn Hm.
rewrite Hn. rewrite Hm.
reflexivity.
Qed.
∀n m : nat, n = 0 → m = 0 → n + m = 0.
Proof.
intros n m Hn Hm.
rewrite Hn. rewrite Hm.
reflexivity.
Qed.
For this theorem, both formulations are fine. But it's important
to understand how to work with conjunctive hypotheses because
conjunctions often arise from intermediate steps in proofs,
especially in bigger developments. Here's a simple example:
Lemma and_example3 :
∀n m : nat, n + m = 0 → n * m = 0.
Proof.
intros n m H.
assert (H' : n = 0 ∧ m = 0).
{ apply and_exercise. apply H. }
destruct H' as [Hn Hm].
rewrite Hn. reflexivity.
Qed.
∀n m : nat, n + m = 0 → n * m = 0.
Proof.
intros n m H.
assert (H' : n = 0 ∧ m = 0).
{ apply and_exercise. apply H. }
destruct H' as [Hn Hm].
rewrite Hn. reflexivity.
Qed.
Another common situation with conjunctions is that we know
A ∧ B but in some context we need just A (or just B)...
Lemma proj1 : ∀P Q : Prop,
P ∧ Q → P.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ? [? ?]. by [].
(*intros P Q HP HQ.
apply HQ.*) Qed.
Lemma proj2 : ∀P Q : Prop,
P ∧ Q → Q.
Proof.
(* WORKED IN CLASS *)
by move ⇒ ? ? [? ?].
(*intros P Q HP HQ.
apply HQ.*) Qed.
P ∧ Q → P.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ? [? ?]. by [].
(*intros P Q HP HQ.
apply HQ.*) Qed.
Lemma proj2 : ∀P Q : Prop,
P ∧ Q → Q.
Proof.
(* WORKED IN CLASS *)
by move ⇒ ? ? [? ?].
(*intros P Q HP HQ.
apply HQ.*) Qed.
Finally, we sometimes need to rearrange the order of conjunctions
and/or the grouping of multi-way conjunctions.
Commutativity and associativity theorems are handy...
Theorem and_commut : ∀P Q : Prop,
P ∧ Q → Q ∧ P.
Proof.
(* WORKED IN CLASS *)
by move ⇒ ? ? [? ?].
(*intros P Q HP HQ.
split.
- (* left *) apply HQ.
- (* right *) apply HP.*) Qed.
P ∧ Q → Q ∧ P.
Proof.
(* WORKED IN CLASS *)
by move ⇒ ? ? [? ?].
(*intros P Q HP HQ.
split.
- (* left *) apply HQ.
- (* right *) apply HP.*) Qed.
In the following proof of associativity, try to use the nested
intro pattern to break the hypothesis...
Theorem and_assoc : ∀P Q R : Prop,
P ∧ (Q ∧ R) → (P ∧ Q) ∧ R.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ? ? [? [? ?]]. by [].
(*
intros P Q R HP [HQ HR].
split.
- (* left *) split.
+ (* left *) apply HP.
+ (* right *) apply HQ.
- (* right *) apply HR.*) Qed.
P ∧ (Q ∧ R) → (P ∧ Q) ∧ R.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ? ? [? [? ?]]. by [].
(*
intros P Q R HP [HQ HR].
split.
- (* left *) split.
+ (* left *) apply HP.
+ (* right *) apply HQ.
- (* right *) apply HR.*) Qed.
Who needs tactics when we have Gallina?
Definition and_comm'_aux P Q (H : P ∧ Q) :=
match H with
| conj HP HQ ⇒ conj HQ HP
end.

We have two parametric propositions here. But we could replace them with universally quantified ones.

Show Proof. (* ==> ?Goal *)
intros P Q R [HP [HQ HR]].
Show Proof. (* ==> (fun (P Q R : Prop) (H : P /\ Q /\ R) => match H with
| conj HP (conj HQ HR) => ?Goal
end) *)
split.
- (* left *) Show Proof. split.
+ (* left *) Show Proof. apply HP.
+ (* right *) Show Proof. apply HQ.
- (* right *) Show Proof. apply HR. Show Proof. Qed.
P ∧ (Q ∧ R) → (P ∧ Q) ∧ R.
Proof.
Show Proof. (* ==> ?Goal *)
intros P Q R [HP [HQ HR]].
Show Proof. (* ==> (fun (P Q R : Prop) (H : P /\ Q /\ R) => match H with
| conj HP (conj HQ HR) => ?Goal
end) *)
split.
- (* left *) Show Proof. split.
+ (* left *) Show Proof. apply HP.
+ (* right *) Show Proof. apply HQ.
- (* right *) Show Proof. apply HR. Show Proof. Qed.
Print or.
(* ===>
Inductive or (A B : Prop) : Prop := or_introl : A -> A \/ B | or_intror : B -> A \/ B *)
The BHK interpretation:
A proof of P ∨ Q is either
This time, let us reverse the order and discuss using disjunction before discussing how to prove it...
The corresponding rule can be written in terms of hypothetical derivations with context:
To use a disjunctive hypothesis in a proof, we proceed by case
analysis, which, as for nat or other data types, can be done
with destruct or intros. Here is an example:
- a pair <a, b> where a is 0 and b is a proof of P, or
- a is 1 and b is a proof of Q.
Disjunction: using it
| Gamma ⊢ A ∨ B Gamma , A ⊢ C Gamma , B ⊢ C | (\/ E) |
| Gamma ⊢ C |
Lemma or_example :
∀n m : nat, n = 0 ∨ m = 0 → n * m = 0.
Proof.
move ⇒ ? ? [Hn | Hm];
by [rewrite Hn | rewrite Hm].
(* Here's a Ltac version ...
(* This pattern implicitly does case analysis on
n = 0 ∨ m = 0 *)
intros n m Hn | Hm.
- (* Here, n = 0 *)
rewrite Hn. reflexivity.
- (* Here, m = 0 *)
rewrite Hm. rewrite <- mult_n_O.
reflexivity.*)
Qed.
∀n m : nat, n = 0 ∨ m = 0 → n * m = 0.
Proof.
move ⇒ ? ? [Hn | Hm];
by [rewrite Hn | rewrite Hm].
(* Here's a Ltac version ...
(* This pattern implicitly does case analysis on
n = 0 ∨ m = 0 *)
intros n m Hn | Hm.
- (* Here, n = 0 *)
rewrite Hn. reflexivity.
- (* Here, m = 0 *)
rewrite Hm. rewrite <- mult_n_O.
reflexivity.*)
Qed.
We can see in this example that, when we perform case analysis on
a disjunction A ∨ B, we must satisfy two proof obligations,
each showing that the conclusion holds under a different
assumption — A in the first subgoal and B in the second.
Note that the case analysis pattern (Hn | Hm) allows us to name
the hypotheses that are generated in the subgoals.
Conversely, to show that a disjunction holds, we need to show that
one of its sides does. Two constructors — two introduction rules!
This is done via two tactics, left and
right. As their names imply, the first one requires proving the
left side of the disjunction, while the second requires proving
its right side.
Here is a trivial example...
Disjunction: proving it
| Gamma ⊢ A | (\/ I_l) |
| Gamma ⊢ A ∨ B |
| Gamma ⊢ B | (\/ I_r) |
| Gamma ⊢ A ∨ B |
Lemma or_intro : ∀A B : Prop, A → A ∨ B.
Proof.
move ⇒ ? ? ?. left. by [].
(*
intros A B HA.
left.
apply HA.*)
Qed.
Proof.
move ⇒ ? ? ?. left. by [].
(*
intros A B HA.
left.
apply HA.*)
Qed.
... and a slightly more interesting example requiring both left
and right:
We need Nat for pred ...
Require Import Nat.
Lemma zero_or_succ :
∀n : nat, n = 0 ∨ n = S (pred n).
Proof.
move ⇒ [|]; by [left|right].
(*
intros |n.
- left. reflexivity.
- right. reflexivity.*)
Qed.
Lemma mult_eq_0 :
∀n m, n * m = 0 → n = 0 ∨ m = 0.
Proof.
(* WORKED IN CLASS *)
move ⇒ [|] ?; first by left.
case ⇒ [|m]; first by right.
(* At this stage, case would produce a warning "Nothing to inject". In previous versions of Coq, it actually produced an error: "This equality is discriminable. You should use the discriminate tactic to solve the goal."*)
discriminate.
Qed.
Theorem or_commut : ∀P Q : Prop,
P ∨ Q → Q ∨ P.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ? [|]; by [right | left].
(*
intros P Q HP | HQ.
- (* left *) right. apply HP.
- (* right *) left. apply HQ.*) Qed.
Lemma zero_or_succ :
∀n : nat, n = 0 ∨ n = S (pred n).
Proof.
move ⇒ [|]; by [left|right].
(*
intros |n.
- left. reflexivity.
- right. reflexivity.*)
Qed.
Lemma mult_eq_0 :
∀n m, n * m = 0 → n = 0 ∨ m = 0.
Proof.
(* WORKED IN CLASS *)
move ⇒ [|] ?; first by left.
case ⇒ [|m]; first by right.
(* At this stage, case would produce a warning "Nothing to inject". In previous versions of Coq, it actually produced an error: "This equality is discriminable. You should use the discriminate tactic to solve the goal."*)
discriminate.
Qed.
Theorem or_commut : ∀P Q : Prop,
P ∨ Q → Q ∨ P.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ? [|]; by [right | left].
(*
intros P Q HP | HQ.
- (* left *) right. apply HP.
- (* right *) left. apply HQ.*) Qed.
Falsehood and Negation
- We could define ¬ P ("not P") as ∀ Q, P → Q.
- Coq actually makes a slightly different choice, defining ¬ P as P → False, where False is a particular contradictory (empty) proposition defined in the standard library.
Print not.
(* ===>
not = fun A : Prop => A -> False
: Prop -> Prop *)
(* ===>
not = fun A : Prop => A -> False
: Prop -> Prop *)
What is False then ??
Print False.
That is, False is an inductive type with no constructors —
i.e., no way to build evidence for it.
If we get False into the proof context, we can destruct it to complete any goal:
Gamma ⊢ False ---------------------- (False E) Gamma ⊢ P
Theorem ex_falso_quodlibet : ∀(P:Prop),
False → P.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? [].
(*intros P contra.
destruct contra.*) Qed.
False → P.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? [].
(*intros P contra.
destruct contra.*) Qed.
The Latin ex falso quodlibet means, literally, "from falsehood
follows whatever you like"; this is another common name for the
principle of explosion.
In Ltac, there is, in fact, a tactic for this.
Theorem ex_falso_quodlibet' : ∀(P:Prop),
False → P.
Proof.
intros ? H. exfalso. apply H.
Qed.
False → P.
Proof.
intros ? H. exfalso. apply H.
Qed.
Exercise: 2 stars, standard, optional (not_implies_our_not)
Show that Coq's definition of negation implies the intuitive one mentioned above:
Fact not_implies_our_not : ∀(P:Prop),
¬P → (∀(Q:Prop), P → Q).
Proof.
(* FILL IN HERE *) Admitted.
☐
¬P → (∀(Q:Prop), P → Q).
Proof.
(* FILL IN HERE *) Admitted.
Negation and falsity: proving it
Theorem zero_not_one : ~(0 = 1).
Proof.
discriminate.
Qed.
Proof.
discriminate.
Qed.
Such inequality statements are frequent enough to warrant a
special notation, x ≠ y:
Check (0 ≠ 1).
(* ===> Prop *)
Theorem zero_not_one' : 0 ≠ 1.
Proof.
discriminate.
Qed.
(* ===> Prop *)
Theorem zero_not_one' : 0 ≠ 1.
Proof.
discriminate.
Qed.
Theorem not_False :
¬False.
Proof.
by move ⇒ [].
Qed.
¬False.
Proof.
by move ⇒ [].
Qed.
Let us have a quick look at the variety of Ltactics tailored for negation and contradiction. First, a pedestrian proof...
Theorem contradiction_implies_anything : ∀P Q : Prop,
(P ∧ ¬P) → Q.
Proof.
move ⇒ ? ? [HP HNA].
apply HNA in HP. by [].
Qed.
(P ∧ ¬P) → Q.
Proof.
move ⇒ ? ? [HP HNA].
apply HNA in HP. by [].
Qed.
We have a contradition in contex, so ssreflect's by sees immediately what's going on. Actually, it's even quicker than that:
Theorem contradiction_implies_anything2 : ∀P Q : Prop,
(P ∧ ¬P) → Q.
Proof.
by move ⇒ ? ? [? ?].
Qed.
(P ∧ ¬P) → Q.
Proof.
by move ⇒ ? ? [? ?].
Qed.
Theorem contradiction_implies_anything3 : ∀P Q : Prop,
(P ∧ ¬P) → Q.
Proof.
intros P Q [hp hnp].
contradiction.
Qed.
(P ∧ ¬P) → Q.
Proof.
intros P Q [hp hnp].
contradiction.
Qed.
Theorem contradiction_implies_anything4 : ∀P Q : Prop,
(P ∧ ¬P) → Q.
Proof.
intros P Q [hp hnp].
contradict hnp. assumption.
Qed.
Theorem contradiction_implies_anything5 : ∀P Q : Prop,
(P ∧ ¬P) → Q.
Proof.
intros P Q [hp hnp].
contradict hnp. done.
Qed.
(P ∧ ¬P) → Q.
Proof.
intros P Q [hp hnp].
contradict hnp. assumption.
Qed.
Theorem contradiction_implies_anything5 : ∀P Q : Prop,
(P ∧ ¬P) → Q.
Proof.
intros P Q [hp hnp].
contradict hnp. done.
Qed.
Theorem contradiction_implies_anything6 : ∀P Q : Prop,
(P ∧ ¬P) → Q.
Proof.
intros P Q [hp hnp].
exfalso.
(* Note assumption would not work here. *)
Fail assumption.
(* done is more powerful. *)
done.
Qed.
(P ∧ ¬P) → Q.
Proof.
intros P Q [hp hnp].
exfalso.
(* Note assumption would not work here. *)
Fail assumption.
(* done is more powerful. *)
done.
Qed.

Note: in the statement of the result below, because of ssreflect conventions, we have to be careful how we treat double negation.
Theorem double_neg : ∀P : Prop,
P → ¬¬P.
Proof.
(* WORKED IN CLASS *)
by move ⇒ ? ? ?.
Qed.
P → ¬¬P.
Proof.
(* WORKED IN CLASS *)
by move ⇒ ? ? ?.
Qed.
Write for yourself a natural deduction proof of double_neg:
Theorem: P implies ~~P, for any proposition P.
Exercise: 2 stars, standard, recommended (contrapositive)
Theorem contrapositive : ∀(P Q : Prop),
(P → Q) → (¬Q → ¬P).
Proof.
(* FILL IN HERE *) Admitted.
☐
(P → Q) → (¬Q → ¬P).
Proof.
(* FILL IN HERE *) Admitted.
Theorem not_both_true_and_false : ∀P : Prop,
¬(P ∧ ¬P).
Proof.
(* FILL IN HERE *) Admitted.
☐
¬(P ∧ ¬P).
Proof.
(* FILL IN HERE *) Admitted.
Equality
Module MyEquality.
Inductive eq {X:Type} : X → X → Prop :=
| eq_refl : ∀x, eq x x.
Notation "x = y" := (eq x y)
(at level 70, no associativity)
: type_scope.
Inductive eq {X:Type} : X → X → Prop :=
| eq_refl : ∀x, eq x x.
Notation "x = y" := (eq x y)
(at level 70, no associativity)
: type_scope.
The way to think about this definition is that, given a set X,
it defines a family of propositions "x is equal to y,"
indexed by pairs of values (x and y) from X. There is just
one way of constructing evidence for each member of this family:
applying the constructor eq_refl to a type X and a value x :
X yields evidence that x is equal to x.
The inductive definition of equality corresponds to Leibniz
equality: what we mean when we say "x and y are equal" is
that every property on P that is true of x is also true of
y.
Lemma leibniz_equality : ∀(X : Type) (x y: X),
x = y → ∀P:X→Prop, P x → P y.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ? ? [].
(* Look what happened ... *)
by [].
Qed.
x = y → ∀P:X→Prop, P x → P y.
Proof.
(* WORKED IN CLASS *)
move ⇒ ? ? ? [].
(* Look what happened ... *)
by [].
Qed.
We can use eq_refl to construct evidence that, for example, 2 =
2. Can we also use it to construct evidence that 1 + 1 = 2?
Yes, we can. Indeed, it is the very same piece of evidence! The
reason is that Coq treats as "the same" any two terms that are
convertible according to a simple set of computation rules.
These rules, which are similar to those used by Compute, include
evaluation of function application, inlining of definitions, and
simplification of matches.
Lemma four: 2 + 2 = 1 + 3.
Proof.
apply eq_refl.
Qed.
Proof.
apply eq_refl.
Qed.
The reflexivity tactic that we have used to prove equalities up
to now is essentially just short-hand for apply refl_equal.
In tactic-based proofs of equality, the conversion rules are
normally hidden. But you can see them
directly at work in the following explicit proof objects:
Definition four' : 2 + 2 = 1 + 3 :=
eq_refl 4.
End MyEquality.
eq_refl 4.
End MyEquality.
Theorem not_true_is_false' : ∀b : bool,
b ≠ true → b = false.
Proof.
move ⇒ [] hp; by [].
(* An old-fashioned Ltac proof:
intros H.
- (* b = false *)
unfold not in H.
exfalso. (* <=== *)
apply H. reflexivity.
- (* b = true *) reflexivity. *)
Qed.
b ≠ true → b = false.
Proof.
move ⇒ [] hp; by [].
(* An old-fashioned Ltac proof:
intros H.
- (* b = false *)
unfold not in H.
exfalso. (* <=== *)
apply H. reflexivity.
- (* b = true *) reflexivity. *)
Qed.
Truth
Print True.
(* ===>
Inductive True : Prop := I : True *)
(* ===>
Inductive True : Prop := I : True *)
This is incorporating the following axiom:
| (True I) | |
| Gamma ⊢ True |
Lemma True_is_true : True.
Proof. apply I. Qed.
Proof. apply I. Qed.
Unlike False, which is used extensively, True is used quite
rarely, since it is trivial (and therefore uninteresting) to prove
as a goal, and it carries no useful information as a hypothesis.
But it can be quite useful when defining complex Props using
conditionals or as a parameter to higher-order Props. We will
see some examples such uses of True later on.
(* Sun Jul 14 22:07:53 MSK 2019 *)


Every HTML element has a default display value depending on what type of element it is. The default display value for most elements is block or inline.
-
Block elements always start on a new line and take
up the full width available. Examples include

and

elements. -
Inline elements do not start on a
new line and only take up as much width as necessary. Any height and
width properties will not affect on this element. Examples include

and
elements.
Fortunately, the default display can be overridden. The Flexbox lets containers decide how to evenly distribute their children including their size and the space between them.


Event
SMS
Menu
Home
Signup
Log In
Sign Up
Image (URL)
Name
Email address
Password
Phone Number
1. What is your favorite type of food?
2. What kind of events are you interested in?
Choose a category
3. What's your zipcode?
4. How far are you willing to travel for restaurants/events? (Up to 25miles)
Radius
Submit
Or login
here


CHRISTY LEE SCHNEIDER
Republican
Southwest Area Security Manager for SAP Software Solutions I begin my employment November 16th, 2020.
I have been in a security leadership role for over 20 years. I had the opportunity to train at the FBI Academy in Quantico, VA. I have also participated in numerous leadership academies. I have a bachelors degree in Political Science.
80130
I have donated to the District Attorney's campaign, 18th Judicial District in 2016.
Member, Colorado Association of Robbery Investigators (CARI) Board Member, ADP iWIN Participant and Assessor, Target Leadership Academy Participant, Comcast Women’s Resource Group COMMUNITY INVOLVEMENT Volunteer, Platte River Academy Foster, 4Paws4 Life
I have been a member of the Colorado Association of Robbery Investigators for over 10 years. I helped fundraise for the organization to offset the costs of training, so it didn't impact their police departments. I have also been a board for the ADP Women in Networking organization, that provides local pet and women's charities in the Denver Metro area.
I want to serve our community. I'm at a point in my career where I have the time and energy to give back. In addition, as a political science major I enjoy getting involved with politics and want to make a difference in Colorado!
As a Director of Client Services at ADP, I developed and cultivated strong relationships with senior leadership, internal partners and team members to influence and ensure standardization of policies and procedures across the market and created a culture of teamwork. I have proven record of generating and building relationships, managing projects from concept to completion and developing and coaching individuals to success. I am skilled in building cross-functional teams, demonstrating exceptional communication skills and making critical decisions during challenges.
As a Director I led a team of remote HR Business Partners/Consultants who delivered Account Management, HCM SaaS, Compliance, Risk Management, Training & Strategic HR Consultation to over 400 clients and managed $35 million in annual controllable revenue. In order to run a successful market I applied analytical and leadership skills to solve all my client service issues.
Female


|
Boost Sorting Algorithm Library
Header <boost/algorithm/sorting/string_sort.hpp>
|
Contents
- Introduction
- Functions
-
- string_sort
- Examples
Introduction
string_sort is a hybrid radix-based/comparison-based algorithm that sorts strings of characters in ascending order.
The simplest version (no functors) sorts strings of items that can cast to an unsigned data type
(such as an unsigned char), have a < operator, and have a size function, such as a std::string.
The functor version can sort any string of discrete elements, via templating, but requires
definitions of a get_char (acts like x[offset] on a string),
get_length (returns length of the string being sorted), and a comparison functor.
Individual characters returned by get_char must support the != operator and have an unsigned
value that defines their lexicographical order.
This algorithm is not efficient for character types larger than 2 bytes each, and is optimized
for one-byte character strings.
For this reason, std::sort will be called instead if the character type is of size > 2.
string_sort has a special optimization for identical substrings.
This adds some overhead on random data, but identical substrings are common in real strings.
reverse_string_sort sorts strings in reverse (decending) order, but is otherwise identical.
Windows/x86 Performance Graph
OSX/G4 Performance Graph
Functions
string_sort
template
inline void string_sort(RandomAccessIter first, RandomAccessIter last,
Unsigned_char_type unused);
template
inline void string_sort(RandomAccessIter first, RandomAccessIter last);
template
inline void reverse_string_sort(RandomAccessIter first,
RandomAccessIter last, Compare comp, Unsigned_char_type unused);
template
inline void reverse_string_sort(RandomAccessIter first,
RandomAccessIter last, Compare comp);
template
inline void string_sort(RandomAccessIter first, RandomAccessIter last,
Get_char getchar, Get_length length);
template
inline void string_sort(RandomAccessIter first, RandomAccessIter last,
Get_char getchar, Get_length length, Compare comp);
template
inline void reverse_string_sort(RandomAccessIter first,
RandomAccessIter last, Get_char getchar, Get_length length, Compare comp);
- Requires:
For the first version of string_sort, the one that takes three arguments:
-
[first, last) is a valid range.
-
RandomAccessIterator is a Random Access Iterator.
-
RandomAccessIterator is mutable.
-
RandomAccessIterator's value type is LessThan Comparable.
-
RandomAccessIterator's value type supports .size(),
which returns the integer length of the value type.
-
RandomAccessIterator's value type supports the [] operator,
which returns an integer data type that is castable to and the same size as Unsigned_char_type.
Given that the leading n - 1 characters are the same for a and b,
(Unsigned_char_type)a[n] < (Unsigned_char_type)b[n] -> a < b.
For the second version of string_sort, the one that takes two arguments:
-
[first, last) is a valid range.
-
RandomAccessIterator is a Random Access Iterator.
-
RandomAccessIterator is mutable.
-
RandomAccessIterator's value type is LessThan Comparable.
-
RandomAccessIterator's value type supports .size(),
which returns the integer length of the value type.
-
RandomAccessIterator's value type supports the [] operator,
which returns an integer data type that is castable to and the same size as an unsigned char.
Given that the leading n - 1 characters are the same for a and b, (unsigned char)a[n] < (unsigned char)b[n] -> a < b.
For the first version of reverse_string_sort, the one that takes three arguments:
-
[first, last) is a valid range.
-
RandomAccessIterator is a Random Access Iterator.
-
RandomAccessIterator is mutable.
-
Compare provides a Strict Weak Ordering.
-
RandomAccessIterator's value type is convertible to
Compares's argument type.
-
RandomAccessIterator's value type supports .size(),
which returns the integer length of the value type.
-
RandomAccessIterator's value type supports the [] operator,
which returns an integer data type that is castable to and the same size as an unsigned char.
Given that the leading n - 1 characters are the same for a and b,
(unsigned char)a[n] > (unsigned char)b[n] -> Compare(a, b).
For the second version of reverse_string_sort, the one that takes four arguments:
-
[first, last) is a valid range.
-
RandomAccessIterator is a Random Access Iterator.
-
RandomAccessIterator is mutable.
-
Compare provides a Strict Weak Ordering.
-
RandomAccessIterator's value type is convertible to
Compares's argument type.
-
RandomAccessIterator's value type supports .size(),
which returns the integer length of the value type.
-
RandomAccessIterator's value type supports the [] operator,
which returns an integer data type that is castable to and the same size as Unsigned_char_type.
Given that the leading n - 1 characters are the same for a and b,
(Unsigned_char_type)a[n] > (Unsigned_char_type)b[n] -> Compare(a, b).
For the third version of string_sort, the one that takes four arguments:
-
[first, last) is a valid range.
-
RandomAccessIterator is a Random Access Iterator.
-
RandomAccessIterator is mutable.
-
RandomAccessIterator's value type is LessThan Comparable.
-
Get_length called on the RandomAccessIterator's value type
returns the integer length in characters of the value type.
-
Get_char called with the RandomAccessIterator's value type
as the first argument and an unsigned integer as the second argument returns the
corresponding unsigned character, such that Get_char(a, n) corresponds to a[n].
Given that the leading n - 1 characters are the same for a and b,
Get_char(a,n) < Get_char(b,n) -> a < b.
For the fourth version of string_sort, the one that takes five arguments:
-
[first, last) is a valid range.
-
RandomAccessIterator is a Random Access Iterator.
-
RandomAccessIterator is mutable.
-
Compare provides a Strict Weak Ordering.
-
RandomAccessIterator's value type is convertible to
Compares's argument type.
-
Get_length called on the RandomAccessIterator's value type
returns the integer length in characters of the value type.
-
Get_char called with the RandomAccessIterator's value type
as the first argument and an unsigned integer as the second argument returns the
corresponding unsigned character, such that Get_char(a, n) corresponds to a[n].
Given that the leading n - 1 characters are the same for a and b,
Get_char(a,n) < Get_char(b,n) -> Compare(a, b).
For the third version of reverse_string_sort, the one that takes five arguments:
-
[first, last) is a valid range.
-
RandomAccessIterator is a Random Access Iterator.
-
RandomAccessIterator is mutable.
-
Compare provides a Strict Weak Ordering.
-
RandomAccessIterator's value type is convertible to
Compares's argument type.
-
Get_length called on the RandomAccessIterator's value type
returns the integer length in characters of the value type.
-
Get_char called with the RandomAccessIterator's value type
as the first argument and an unsigned integer as the second argument returns the
corresponding unsigned character, such that Get_char(a, n) corresponds to a[n].
Given that the leading n - 1 characters are the same for a and b,
Get_char(a,n) > Get_char(b,n) -> Compare(a, b).
- Postconditions: The elements in the range [first, last) are sorted in ascending order.
- Complexity:
O(N * mean_string_length) character comparisons worst-case performance,
where N is last - first.
- Rationale:
This provides a general-case string-sorting algorithm that
takes asymptotically less time than is possible for a pure comparison-based algorithm.
Why use recursion for string_sort instead of a stack,
like American Flag Sort?
Because recursion is simpler, more readable, and has comparable performance.
The stacksize limitation is not a serious issue on common modern systems.
Examples
Simple string sorting
Wide-character string sorting
Sorting a structure on a string key
Sorting in reverse order
Sorting in reverse order with functors
Sorting with functors
vector<string> vec;
vec.push_back("c");
vec.push_back("ab");
vec.push_back("a");
string_sort(vec.begin(), vec.end());
//The sorted vector contains "a ab c"
Reverse order:
struct greaterthan {
bool operator()(const DATATYPE &x, const DATATYPE &y) const
{ return x > y; }
};
reverse_string_sort(vec.begin(), vec.end(), std::greater<string>());
//The sorted vector contains "c ab a"
Structure:
struct data_type {
string a;
inline bool operator<(const data_type &y) const { return a < y.a;}
};
vector<data_type> vec;
struct bracket {
unsigned char operator()(const data_type &x, size_t offset) const { return x.a[offset]; }
};
struct getsize {
size_t operator()(const data_type &x) const{ return x.a.size(); }
};
string_sort(vec.begin(), vec.end(), bracket(), getsize());
Revised
04
December, 2006
Copyright © 2009 Steven Ross
Distributed under the Boost Software License, Version 1.0. (See
accompanying file LICENSE_1_0.txt or
copy at http://www.boost.org/LICENSE_1_0.txt)


Connection Class
Connection with a remote process
Instances of this class represent a connection with a remote monitor process. The remote process is a peer of this process - it may produce and/or consume probe information.
This is an internal class created when a connection to a server is requested from a monitor, or when an external connection is made from a Server instance.
Constructor
Connection
-
model
Parameters:
-
model
Object- Initial data model. Can be a JS object or another Model.
-
[hostName]
String optionalThe host name to connect with. Used if url isn't present.
-
[hostPort]
Number optionalThe host port to connect using. Used if url isn't present.
-
[url]
String optionalThe URL used to connect. Built if hostName is supplied.
-
[socket]
Io.socket optionalUse this pre-connected socket instead of creating a new one.
-
[gateway=false]
Boolean optionalAllow this connection to use me as a gateway? See
Router.setGateway()
-
[firewall=false]
Boolean optionalFirewall inbound probe requests on this connection?
-
[remoteHostName]
String READONLY optionalHost name given by the remote server.
-
[remoteAppName]
String READONLY optionalApp name given by the remote server.
-
[remoteAppInstance]
Integer READONLY optionalThe remote application instance ID running on the host.
-
[remotePID]
String READONLY optionalRemote process ID.
-
[remoteProbeClasses]
Array of String READONLY optionalArray of probe classes available to the remote server.
-
[remoteGateway]
Boolean READONLY optionalCan the remote process act as a gateway?
-
[remoteFirewall]
Boolean READONLY optionalIs the remote side firewalled from inbound probe requests?
Item Index
Methods
Events
Methods
addEvent
-
eventName
-
handler
Bind the specified handler to the remote socket message.
Only a single handler (per message name) can be bound using this method.
Parameters:
-
eventName
StringThe event name to handle
-
handler
Function (args..., callback)Called when the message is received.
- args... {Mixed} Arguments sent in by the remote client
- callback {Function} Final arg if the client specified a callback
disconnect
-
reason
Disconnect from the remote process
This can be called from the underlying transport if it detects a disconnect, or it can be manually called to force a disconnect.
Parameters:
-
reason
StringReason for the disconnect
emit
-
name
-
args...
-
callback
Emit the specified message to the socket.
The other side of the connection can handle and respond to the message using the 'on' method.
isThisHost
-
hostName
Is this connection with the specified host?
Parameters:
-
hostName
StringThe host name to check
Returns:
List
-
[items]
Constructor for a list of Connection objects
var myList = new Connection.List(initialElements);
Parameters:
-
[items]
Array optionalInitial list items. These can be raw JS objects or Connection data model objects.
Returns:
ping
-
callback
Ping a remote connection
Parameters:
-
callback
Function(error)Callback when response is returned
probeConnect
-
monitorJSON
-
callback
Process an inbound request to connect with a probe
This will fail if this connection was created as a firewall.
Parameters:
-
monitorJSON
ObjectProbe connection parameters, including:
-
callback
Function(error, probeJSON)Callback function
probeControl
-
params
-
callback
Process an inbound control request to a probe
Parameters:
-
params
ObjectControl parameters, including: probeId {String} The unique probe id name {String} The control message name params {Object} Any control message parameters
-
callback
Function(error, returnParams)Callback function
probeDisconnect
-
params
-
callback
Process an inbound request to disconnect with a probe
Parameters:
-
params
ObjectDisconnect parameters, including: probeId {String} The unique probe id
-
callback
Function(error)Callback function
Events
connect
Connected to remote monitor process
This event is emitted after the two sides of the connection have exchanged information about themselves.
disconnect
Disconnected from a remote monitor process
This event is emitted after the remote connection is disconnected and resources released.
Event Payload:
-
reason
StringReason for the disconnect


Here's a Escape game:
Here's a short trivia:
Here's a 6 minute video showing how to make a mother's day card!:
Click here to do a fun virtual Star Wars themed escape room.


---
layout: post
title: links for 2007-03-27
date: 2007-03-27 00:00:00
---
-
"The problems surrounded privacy and cost. Paying for each fetch of location data quickly makes any tracking application infeasible."
-
"It doesn’t take much to go from typing to stereotyping–”Sysadmins want these kinds of features”–and once that happens, empathy is lost."
-
"What the company plans to do is load its software onto handsets running the Symbian, Windows Mobile and Palm OS's. It will then track every kind of activity which could be pertinent to collating data for advertising feedback."


Power Hour for
Deadline is today!
Tasks to work on
Number of tasks to show
Personal
Deadline is today!
Tasks to work on
Number of tasks to show


Week 3 Web Basics Assignment
Battleship Game
Battleship.pdf is attached in this repository check the specifications there or in index.js also


rootkit
`Prev `__
R
`Next `__
--------------
**rootkit**: /root´kit/, n.
[very common] A kit for maintaining `*root* `__; an automated
`*cracking* <../C/cracking.html>`__ tool. What `*script
kiddies* <../S/script-kiddies.html>`__ use. After a cracker has first
broken in and gained root access, he or she will install modified
binaries such as a modified version login with a backdoor, or a version
of ps that will not report the cracker's processes). This is a rootkit.
--------------
+------------------------------+----------------------------+--------------------------+
| `Prev `__ | `Up <../R.html>`__ | `Next `__ |
+------------------------------+----------------------------+--------------------------+
| root mode | `Home <../index.html>`__ | rot13 |
+------------------------------+----------------------------+--------------------------+


Department of Advanced Science and Technology
University of Computer Studies
B.C.Sc/B.C.Tech. ( Fifth Year)
Computer System Fundamentals(CT-503)
Mid Tearm Examination
March, 2015
Zone III
Answer ALL Questions
Time allowed 3hours.
-
- Define three instruction types and build a datapath in operation for (sub $t1, $t2, $t3) instruction.(10 marks)
- In this problem we have four instructions: lad (lw), store (sw), R-type (add, sub, and or, slt) and branch (beq). Compare the average time between instuctions of a sigle-cycle implementation, in whcih all instructions take one clock cycle to a pipelined implementation. The operation times for the major functional units in this problem are 100ps for menory access, 100ps for ALU operatin and 50ps for register file read or write. Compare the average time between instructions of a single-ccle and pipelined implementation for one million load instructions.(10 Marks)
-
- What are the pipeline hazards? Define each hazard with sample instructions.(10 marks)
- Describe the pipelined dependences in the following five instructions equence using simplified datapaths to shw the dependences and how to solve the hazard in the pipelined registers?(10 marks)
sub $2,$1,$3
and $12,$2,$5
or $13,$6,$2
add $14,$2,$2
sw $15,100($2)
-
- Explain dynamic pipeline scheduling with three primary units.(10 Marks)
- What is the cache?Describe about the cache types.(10 Marks)
-
- Assume there are three small caches, each consiting of four one-word blocks. Find the number of misses for each cache organization given the following sequence of block address: 0,4,0,6, 10, 4 and 0.(10 marks)
- How to design the memory systm to support caches. Explain that wich organization is better than others? Assume
-1 memory bus clock cycle to send the address
-15 memory bus clock cycles for each DRAM access initiated
-1 memory bus clock cycle to send a word of data(10 Marks)
-
- Suppose we have a processor with a base CPI of 1.0, assuming all references hit in the primary cache, and a clock rate of 5 GHz. Assume a main memory access time of 100ns, including all the miss handling. Suppose the miss rate per instruction at the primary cache is 2%. How much faster will the processor be if we add a secondary cache that has a 5ns access time either a hit or a miss and is large enough to reduce the miss rate to main memory to 0.5%?(10 Marks)
- Explain about the virtual memory. Compute the total page table size when there are 4 KB pages and 4 bites per page table entry, assuming 32-bit vitrual address.(10 Marks)


Lottery winners from last 25 years explain what they've done with their millions
Lottery winners from each of the last 25 years were brought together by Camelot to celebrate the first ever draw on November 19, 1994 - here we look at their astonishing stories
by Jeremy Armstrong, Adam Aspinall, https://www.facebook.com/dailymirror/, https://www.mirror.co.uk/authors/adam-aspinall/This may be the luckiest group of people in Britain.
They are 25 lottery winners from 25 consecutive years, brought together by Camelot to celebrate the first ever draw on November 19, 1994.
The winners have been pictured by celebrity photographer Sven Arnstein.
Since it began a whopping £71 billion in prize money has been paid to UK winners across all National Lottery games creating than 5,500 millionaires and multi-millionaires.
Currently, seven millionaires are made in an average week across all National Lottery games.
Here are their remarkable stories...
1995: Elaine Thompson, 63, of Killingworth, Tyne and Wear, won £2,704,666
Shares a four-bedroom detached house with husband Derek, 61.
“I kept a journal for my children since they were born and it tells the story of the Lottery win and how it changed our lives.
"They had to work throughout their teens and seeing them go to university and buy their own houses – with much of their own savings – was a defining moment for me.
1996: Deana Sampson, 58, of Sheffield, South Yorks, won £5,439,681
She has two children and two grandchildren.
“I had £3.60 in my bank account when I won, and life was a real struggle.
"I bought my parents a bungalow and took 22 family members on a luxury holiday to Jamaica.
"I spent £800,000 on a yacht on my 40th birthday.”
1997: Cheryl Brudenell, 52, of Stockton-on-Tees, won £916,915
She has two children and lives with husband Mark, 54.
“The Lottery win has allowed me to indulge in my passion for Robbie Williams, but I’ve never totted up how much it has cost to see him around 40 times in concert, in places as far flung as Barcelona, Vegas, Berlin and Belgium.”
1998: Viv Moss, 68, of Newquay, Cornwall, won £6,048,499
Lives with husband Kevin, 73, and has two children.
“The shock of winning was like an unexpected death. I had sickness and diarrhoea for a fortnight, and lost a stone in weight, going from a size 16 to a 12.
"I taught hair and beauty at a local college, but I couldn’t let the class down, so I carried on working for eight months until the end of their course.
"We went from a four-bed home to a five-bed, and drove our Ford Escort to a Range Rover showroom.
"The salesman was called Rupert and when we told him we’d pay cash, he said ‘You’ve either just won the Lottery, or sold a business.’
"We told him we had hit the jackpot. I swapped my eight-year-old Ford Focus for a convertible, but the dog didn’t like the wind in his ears, so I later chose a Bentley instead.”
1999: Sam Lange, 47, from Seaford, won £1,575,878
She lives with partner Malcolm and has three children as well as a stepson.
“When I won the Lottery, I had been saving £50 a week to go and see my dad in New Zealand, after four years apart. We were raising my partner’s son and I was working weekends while Malcolm worked shifts.
"We were suddenly able to visit Dad for a month and take him to places he’d never dreamed like flying up a mountain and swimming with dolphins.
"It was a £5,000 trip but worth every penny. We stayed in the same house, built an extension and had three children of our own.
"We also bought a holiday home in France which has given us many happy family holidays together. I was able to give up work, and devote myself to being a mum.”
2000: Ray Wragg, 81, from Sheffield, won £7,649,520
He lost his wife Barbara last year and lives in the five-bed bungalow she chose after their win.
“The morning after I won the Lottery, I rang my boss to resign. When I told him I’d had a win, he said ‘That reminds me, I need to check my ticket.’ I said ‘Don’t bother Dave – I won the lot!’
"I had never been out of the country when we won the Lottery, and I didn’t even own a passport.
"My wife Barbara didn’t like flying, so we’d been on holiday to Torquay for 31 years on the trot.
"After winning, we decided to try a cruise and we loved it. We bought a Range Rover, and filled it with Easter Eggs for the local kids from a school in Sheffield, and paid for them to have a holiday at a farm.
"I’ll never forget, they had never seen rabbits or guinea pigs – and they were scared. I read about a local boy whose bike had been stolen, and I delivered him a new mountain bike. The look on his face was perhaps my happiest Lottery moment.”
2001: Tom Naylor, 64, from Wheaton Aston, Staffs, won £15,528,286
He lives with wife Rita, 62, in a four-bed barn conversion.
“I was absolutely convinced I’d win the Lottery one day, and I’d tell my friends ‘When my numbers come up, I’ll get a car for every day of the week.’
"Now, I have two Aston Martins, three Jaguars, a Ford Mustang and a Land Rover Discovery. Not bad considering my old car was a Ford Granada.
"My biggest extravagance was flying nine family members to New York via Concorde. It cost £25,000 and when we saw three giant white stretch limos waiting for us outside the airport, it was an incredible moment.
"When we arrived at the hotel, all the tourists pulled their cameras out because they thought we were famous. I felt ten foot tall.”
2002: Sarah Ibbetson, 41, from Leeds, won £3,013,767
She lives with husband Aldan and their three children.
“I was on maternity leave as a dental nurse when we won, and our daughter Alicia was six months old.
"It meant I could be a stay-at-home mum for her, and our other two children who arrived later.
"We were only 24 when we won, and the first things we bought were a Mercedes and a Porsche.
"We went into the car showroom, and when the guy asked how we’d pay, and we said debit card, his face was a picture.
"We made it onto the Sunday Times Rich List, and we’ve still got a copy, with our name at the bottom.
"We went from a three-bed semi to a five-bed detached, and started our own number plate business which we run together in our office.”
2003: Trish Emson, 49, from Rotherham, won £1,747,728
She lives with partner Graham Norton and son Benjamin.
“We had been saving for IVF after trying for five and a half years for a baby, and I lost four stone in weight because I wanted to qualify for the treatment.
"I was due to start fertility treatment in January, and I was so happy when we won, because I knew we could afford more attempts if our first didn’t work.
"A few weeks after our win, we were invited to an England Rugby game, but the champagne made me feel sick. Two weeks later, we discovered I was pregnant, and Benjamin was born in August.
"It was like winning the Lottery all over again. We bought him a babygro which said ‘Millionaire in training.’ Our greatest moment was flying Benjamin to Lapland when he was eight – and seeing the look on his face when he met Santa.”
2004: Ben Woods, 38 from Liverpool, won £2,485,736
He lives with wife Leanne and their three children.
“I was 23, single and living at home when I won. I finished my shift as a railway guard, and went to the local pub. Mum and dad were sitting there, white with shock, because they’d checked my numbers.
"Dad said he needed to talk to me alone in the toilets, and I thought ‘What have I done?’ I was sure I was about to be told off.
"The money has paid for 12 trips to New York, holidays for my mum and dad, a house for my sister and a five-bed house for me.
"I met my future wife nine months after the win, and when I turned up to collect her for our first date in a brand new Range Rover, her Nan said ‘I think he’s a drug dealer!’
"Now, we have three children and I’m a stay at home dad. My life has totally changed – for the better.”
2005: Sarah Cockings, 36, from Whitley Bay, won £3,045,705
She lives with her partner and three children.
“My eldest son is six, and he tells everyone I won the Lottery. He came home from school and said ‘I told my teacher you won the jackpot and she was laughing.’
"I bought my house outright, and I have a nice car but I live a very normal life. I went back to university to study after winning, because my Mum so wanted that picture of me graduating – which she has now on her mantelpiece.
"My sisters and I live just seven minutes from each other, and our children are all best friends. Just after I won, I bought my two sisters boob jobs, and everyone remembers that.
"But now I’ve had one myself, because mine were wrecked by breastfeeding. Now, it’s my two-year boob birthday. I love them!”
2006: Mother-of-three Geraldine Bradley, 50, won £3,570,063 as part of a family syndicate
She lives in Gwynnon, Llanarthne, south-west Wales with husband Christopher, 48.
“My first thought when I realised I’d won was I wanted to get my ironing done before the press came around. I remember thinking ‘The house needs to be ship shape!’
"The first thing we actually bought was a £9.99 Kentucky Fried Chicken to celebrate, although our first big purchase was a new Mercedes some four months later.
"We moved to a four-bedroom country home with three reception rooms, a snooker room, a maze in the grounds and a lake at the bottom, with geese.
"We’ve been able to support our children as they have grown-up and go on some amazing trips around the World.”
2007: Kerri-Ann Robinson, 41, won £2,543,691
She lives in Stevenage, Herts, with husband Tony and two children.
“I was a mature student studying for a diploma in business at college when my daughter, who was three, begged me for a blackcurrant juice.
"I rushed out on the Wednesday lunchtime, bought her the juice and as an afterthought, chose a Lucky Dip for the Lotto draw that night.
"I checked the numbers the next day at college, during break, and when I realised I had won, everything went blurry.
"I put my ticket in my pencil case, rang my mum and burst into tears. She thought something terrible had happened.
"I went from wearing costume jewellery to buying the real thing. I married Tony in 2010 in a dream wedding – and walking down the aisle was one of the most magical moments of my life.”
2008: Tracy Field, 51, won £2,561,513
She lives in a four bedroom house in Benfleet, Essex. She has two grown-up sons.
“I had been struggling as a single mum with three jobs, servicing vending machines, cleaning and delivering catalogues, when I was diagnosed with cancer.
"2007 was my lowest year, because I felt so ill, and I lost my long hair. I won the following year, just as I was beginning to get my life back.
"I realised I had won late at night, and I felt compelled to go and buy something, after years of scrimping.
"I went to Tesco at Midnight in my pyjamas, and bought a box of Bonio dog biscuits, because I couldn’t think of what else to buy. I went from a three-bed semi to a four-bed detached, which cost £430,000.
"I’ve also helped my two sons out with homes, but the best thing I spend money on is private medical treatment. I found some more lumps, and instead of waiting, I was able to have scans instantly to put my mind at rest.”
2009: Brian Caswell, 84, from Bolton, won £24,951,269.40 on EuroMillions
He lives in a five-bedroom detached home in Bolton with wife Joan, 82.
“I went to collect the newspapers, and I checked my ticket at the same time.
"I had all six numbers, and I walked home a little in shock. When I got to my gate, the neighbour Stan said ‘Have you heard? A grey haired bloke who lives locally has won the Lottery!’
"We’d lived in that house for 48 years, but after we won, it was clear we’d have to move. We bought ourselves a house, and a house for each of our adult daughters, all in the same day.
"Our favourite moment has been taking our grandchildren to Lapland on a private plane.
"Five years ago, I needed an emergency quadruple by-pass, and instead of waiting, our daughter researched the top surgeon and I paid to go private – so the Lottery has kept me healthy as well as happy.
"Joan and I have just celebrated our Diamond wedding anniversary and feel very lucky in life; i even won a tenner last week!”
2010: Susan Herdman, 51, from Boroughbridge, Yorkshire, won £1, 182,714
She lives with farmer partner Andrew.
“I was a single parent, raising my son Jake and turning down the thermostat because I couldn’t afford the bills, when I won. I think I immediately turned the heating up, and I realised I’d never be cold again.
"I owned a hair salon and I carried on for nine months after I won.
"It was a lightbulb moment. I sold my salon two days later and never looked back.
"I turned to my hobby of Autograss racing, and won the national championships in 2016 and 2017.
"I’ve also done a skydive, ridden in a cowboy ranch and completed the longest zipwire in Europe.”
2011: Geoffrey Bennette, 70, won £3,530,707
He lives near Blackburn with wife Hilary, 63.
“I had recently retired as a manager at Bolton Council. I discovered we’d won early on the Sunday morning, but as I was volunteering at a cycling event for the day I left the ticket at home before contacting Camelot.
"As we love travelling by train, we’ve since explored South Africa, Scandinavia, India, New Zealand and Australia. Whilst in Australia, celebrating our 40th wedding anniversary, we visited Uluru (Ayres Rock) when a rainbow appeared.
"It was a magical moment, so rare even the tour guides ran off the buses with their cameras.
"You can’t put a price on the experiences we’ve had and memories we’ve made.”
2012: Libby Elliot, 57 from Aberdeenshire, won £2,159,664
An empty nester now her four children have left home, she is currently buying a new house.
“My dad gave me the money for my Lotto ticket. I’d taken his grandchildren to visit him in hospital, and he handed them pocket money then gave me two pounds pocket money, on a whim, I put it on the Lucky Dip on my way home.
"The day after I won, Dad had an appointment at the fracture clinic after a fall. I took him to hospital, and he turned and said ‘Look at you. You’re a multi-millionaire and yet you’re sitting here beside me.’
"That still makes me cry. Dad died just before last Christmas, and now my four children have left home, I’m travelling the world on dream trips, from Jerusalem to Route 66 to Buenos Aires.
"I’ve lost 11 stone in total since winning and I’m fitter than I’ve ever been. I bit my nails before I won the Lottery, but now I have beautiful sparkly nails and I love my regular manicures.”
2013: Dione Buss, 53, from Somerset, won £1,888,630
She lives in Bridgwater, Somerset with husband Richard, 54.
“I was diagnosed with Multiple Sclerosis when our daughter Harriet was a baby, and I realised I couldn’t do up the poppers on her babygro.
"I had up to four relapses a year, but the worst was when Harriet was 13, and I ended up paralysed in hospital for a week.
"Thankfully, I responded to steroids but our daughter had to help me onto the toilet and into the bath. No child should have to face that.
"I had just returned to work for the local council after months of sick leave when I won the Lotto jackpot. It improved my health – because my condition can be made worse by stress and exhaustion.
"Richard and I went to see the Great Wall of China, which had been his childhood dream – and standing there, we both became really emotional.
"It really hit home at that moment that our lives had changed. Our daughter has just got married, and we have had an amazing weekend of wedding celebrations.
"Other goosebump moments are our incredible worldwide travel adventures.”
2014: Matt Myles, 33, from from Hereford, won £1,000,000 on the EuroMillions Raffle
He lives in a converted chapel with pregnant wife Stacy and their son.
“I actually had a panic attack when the man from Camelot arrived with the cheque. I was a single lad and I immediately quit my job and flew to Bali on holiday with seven of my mates.
"It was the first of many lads’ holidays - but then I met Stacy, who knocked me for six.
"She was so un-materialistic, and she worked as a play therapist with children. We planned a world trip together, but when we got to China, Stacy became unwell.
"I took her to hospital, where they ran tests but nobody spoke English.
"Finally, they took us into the room, flashed up a baby scan and all the doctors started clapping. I looked at the screen and became so emotional – I actually had my second panic attack.
"Our son was born in December 2017, and now our second baby is due. We live in a converted chapel and I’m buying extra land for a football pitch for my sons.”
2015: Anne Canavan, 58, from Northern Ireland, won £1,054,000 on EuroMillions
“I was washing my car on the afternoon of the draw, and I said to my neighbour ‘It’s about time someone from around here won the Lottery.’
"Normally, I always waited a week before checking my Lottery numbers, but that night, at 1.00am, I suddenly had the urge to check the results, so I switched my laptop on.
"When I realise I’d won, I woke my daughter up, but it took half an hour to convince her that I wasn’t joking.
"After that, we stayed up all night with cups of tea, planning what to do with the money. I still live in the same four-bed house I had before I won. I spent £50,000 doing it up, and I bought four further properties as investments.
"Winning Euromillions has given me the freedom to design and invent new products and I have 17 innovations currently in development.”
2016: Jamie Heavens, 26, from Bournemouth, won £1,000,000 on a Millionaire Riches Scratchcard
He lives with his wife Danielle and their young son.
“I was working as a roofer for the family firm when my uncle sent me to refuel the truck. The first petrol station didn’t do fuel cards, so I drove to another, and then the man in front of me bought a scratch card, so I picked the same card as him.
"I drove to a layby to scratch it, and realised I’d won. But it was 7.30 in the morning, and I still had a day’s shift ahead.
"I couldn’t get signal, so I climbed onto the roof we were working on, and rang Camelot. I won a million pounds and earned another £100 for my shift.
"My son Hughie was nine weeks old, and although I’d already proposed to Danielle, and the win gave us the day of our dreams.
"The wedding cost £25,000 but we had a band, a videographer and a massive marquee.
“I was living on a council estate, struggling to raise four children – two of whom were autistic – I was in debt and on benefits.
"Then I won, and I bought a house outright just five minutes up the road, near the special school my children attend. I rang to cancel my benefits and the lady nearly dropped the phone when I said I’d won the Lottery.
"One of the best things I’ve been able to do is send my son, who struggles socially, to private school. He’s no longer bullied and he’s now on the rugby team.
"Meanwhile I paid £7,000 for a gastric sleeve last year. I was nearly 17 stone, and I’m now 11, and I went from almost size 20 to a 12. I love buying new clothes.
"I also bought a car, two houses and a holiday home, but it’s the weight loss and being able to support my children which have changed my life the most.”
2018: Arron Walshaw, 33, won £1,000,000 on Lotto
He lives in Ossett, West Yorkshire, with fiancé Ceri, 24, and their two young children.
“When I saw my ticket stuck to the fridge door by a magnet, and decided to check the results on the app, I thought I’d been pranked.
"When we realised it was true, we went straight onto RightMove to look for a new house.
"We found our dream home three weeks later. Just one month after the win, we conceived our second baby together – and it felt like winning the Lottery all over again.
"We called our new daughter Lottie. I’m a plasterer and I still work, but I’m around to be hands on with the children too.”
2019: Natalie Metcalf, 38, from Thornbury, South Glos, won £1,000,000 on EuroMillions
She lives with fiancé Andy Symes, 41, and their two children.
“I was eight months pregnant when I won, and I could only have a few tiny sips of champagne that night.
"The next day, we went to view a new house and I went into labour a month early. I’m convinced it was the shock.
"Our daughter was born on 5 February, and holding her in my arms was one of the happiest moments of my life. Andy’s dad is one of four boys, Andy is one of three boys, he also has two nephews plus we already had a son, Noah.
"So having a little girl felt like all my dreams had come true – and we called her Poppy Marie Lottie, in honour of our win.
"She was just two weeks old when we went to view more houses – and we bought one, and filled it with brand new furniture.
"Next year, we’re getting married and our happiness will be complete.”