oysteikt/sf1
0
0
Fork 0
forked from oysteikt/sf1-template
Code Pull Requests Activity

Complete Tactics.v

Browse Source
This commit is contained in:
Oystein Kristoffer Tveit
2026-07-08 04:28:06 +09:00
parent c37ed8fc9b
commit e4fac37928
1 changed files with 290 additions and 39 deletions
Download Patch File Download Diff File Expand all files Collapse all files
Tactics.v
+290 -39
View File
@@ -77,7 +77,26 @@ Theorem silly_ex : forall p,
even p = true ->
odd (S p) = true.
Proof.
(* FILL IN HERE *) Admitted.
intros p HevenS Hodd Heven.
apply Hodd.
apply HevenS.
apply Heven.
Qed.
Theorem silly_ex' : forall p,
(forall n, even n = true -> even (S n) = false) ->
(forall n, even n = false -> odd n = true) ->
even p = true ->
odd (S p) = true.
Proof.
intros p HevenS Hodd Heven.
rewrite -> Hodd.
reflexivity.
rewrite -> HevenS.
reflexivity.
rewrite -> Heven.
reflexivity.
Qed.
(** [] *)
(** To use the [apply] tactic, the (conclusion of the) fact
@@ -108,11 +127,17 @@ Proof.
that theorem as part of your (relatively short) solution to this
exercise. You do not need [induction]. *)
Search (rev ?l).
Theorem rev_exercise1 : forall (l l' : list nat),
l = rev l' ->
l' = rev l.
Proof.
(* FILL IN HERE *) Admitted.
intros l l' H.
rewrite H.
symmetry.
apply rev_involutive.
Qed.
(** [] *)
(** **** Exercise: 1 star, standard, optional (apply_rewrite)
@@ -195,7 +220,11 @@ Example trans_eq_exercise : forall (n m o p : nat),
(n + p) = m ->
(n + p) = (minustwo o).
Proof.
(* FILL IN HERE *) Admitted.
intros n m o p eq1 eq2.
transitivity m.
apply eq2.
apply eq1.
Qed.
(** [] *)
(* ################################################################# *)
@@ -286,7 +315,14 @@ Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
j = z :: l ->
x = y.
Proof.
(* FILL IN HERE *) Admitted.
intros X x y z l j H1 H2.
injection H1 as H3 H4.
rewrite H3.
rewrite <- H4 in H2.
injection H2 as H5.
symmetry.
apply H5.
Qed.
(** [] *)
(** So much for injectivity of constructors. What about disjointness? *)
@@ -335,7 +371,9 @@ Example discriminate_ex3 :
x :: y :: l = [] ->
x = z.
Proof.
(* FILL IN HERE *) Admitted.
intros X x y z l j H.
discriminate H.
Qed.
(** [] *)
(** For a more useful example, we can use [discriminate] to make a
@@ -469,13 +507,20 @@ Proof.
(** **** Exercise: 3 stars, standard (nth_error_always_none) *)
Search nth_error.
(** Use [specialize] to prove the the following lemma, following the
model of [specialize_example] above. Do not use [induction]. *)
Lemma nth_error_always_none: forall (l : list nat),
(forall i, nth_error l i = None) ->
l = [].
Proof.
(* FILL IN HERE *) Admitted.
intros l H.
specialize H with (i := 0).
destruct l.
- reflexivity.
- discriminate.
Qed.
(** [] *)
(** Using [specialize] before [apply] gives us yet another way to
@@ -654,7 +699,20 @@ Proof.
Theorem eqb_true : forall n m,
n =? m = true -> n = m.
Proof.
(* FILL IN HERE *) Admitted.
intros n.
induction n as [| n' IHn].
- intros m H.
destruct m as [| m'] eqn:E.
+ reflexivity.
+ discriminate.
- intros m H.
destruct m as [| m'] eqn:E.
+ discriminate.
+ f_equal.
apply IHn.
simpl in H.
apply H.
Qed.
(** [] *)
(** **** Exercise: 2 stars, advanced, optional (eqb_true_informal)
@@ -663,6 +721,34 @@ Proof.
hypothesis explicitly and being as explicit as possible about
quantifiers, everywhere. *)
(* Theorem: for all n m : nat, n =? m = true -> n = m.
Proof: by induction on n.
First, consider the base case where n = 0.
Let's consider the case where m = 0. Then we can substitute (n =? m)
into (0 =? 0), which is always true.
Next, lets consider the case where m = S m' for some nat m'. Then the premise
become (0 =? S m'), which is a contradiction.
Now we consider the inductive case where n = S n' for some natural number n'.
We have the following induction hypothesis:
forall m, (n =? m) = true -> n = m.
And we need to show that S n' = m.
Clearly, m can not be 0, as this would be a contradiction. Lets consider the case
where m = S m' for some natural number m'. We can now infer that
S n' = S m' -> n' = m'
Using the induction hypothesis, we know that this is the case if (n' =? m') is true,
which is immediate from the premise of the theorem. Qed.
*)
(* FILL IN HERE *)
(* Do not modify the following line: *)
@@ -677,7 +763,22 @@ Theorem plus_n_n_injective : forall n m,
n + n = m + m ->
n = m.
Proof.
(* FILL IN HERE *) Admitted.
intros n.
induction n.
- intros m H.
destruct m.
+ reflexivity.
+ discriminate.
- intros m H.
destruct m.
+ discriminate.
+ f_equal.
simpl in H.
rewrite <- plus_n_Sm in H.
rewrite <- plus_n_Sm in H.
injection H.
apply IHn.
Qed.
(** [] *)
(** The strategy of doing fewer [intros] before an [induction] to
@@ -827,7 +928,20 @@ Theorem nth_error_after_last: forall (n : nat) (X : Type) (l : list X),
length l = n ->
nth_error l n = None.
Proof.
(* FILL IN HERE *) Admitted.
intros n X l.
generalize dependent n.
induction l.
- intros n H.
reflexivity.
- intros n H.
simpl in H.
destruct n as [| n'] eqn:Heq.
+ discriminate.
+ simpl.
specialize IHl with (n := n').
injection H.
apply IHl.
Qed.
(** [] *)
(* ################################################################# *)
@@ -1015,7 +1129,28 @@ Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
Proof.
(* FILL IN HERE *) Admitted.
intros X Y l l1 l2 Hsplit.
generalize dependent l2.
generalize dependent l1.
induction l.
- intros l1 l2 Hsplit.
simpl in Hsplit.
injection Hsplit.
intros Hl2 Hl1.
rewrite <- Hl2, <- Hl1.
reflexivity.
- intros l1 l2 Hsplit.
destruct x as [x1 x2].
simpl in Hsplit.
destruct (split l) as [l1' l2'].
injection Hsplit.
intros Hl2 Hl1.
rewrite <- Hl2, <- Hl1.
simpl.
rewrite IHl.
+ reflexivity.
+ reflexivity.
Qed.
(** [] *)
(** The [eqn:] part of the [destruct] tactic is optional; although
@@ -1089,7 +1224,23 @@ Theorem bool_fn_applied_thrice :
forall (f : bool -> bool) (b : bool),
f (f (f b)) = f b.
Proof.
(* FILL IN HERE *) Admitted.
intros f b.
destruct (f b) eqn:Hfb.
- destruct b.
+ rewrite Hfb.
rewrite Hfb.
reflexivity.
+ destruct (f true) eqn:Hft.
* apply Hft.
* apply Hfb.
- destruct b.
+ destruct (f false) eqn:Hff.
* apply Hfb.
* apply Hff.
+ rewrite Hfb.
rewrite Hfb.
reflexivity.
Qed.
(** [] *)
(* ################################################################# *)
@@ -1176,7 +1327,17 @@ Proof.
Theorem eqb_sym : forall (n m : nat),
(n =? m) = (m =? n).
Proof.
(* FILL IN HERE *) Admitted.
intros n.
induction n as [| n' IHn].
- intros m.
destruct m.
+ reflexivity.
+ reflexivity.
- intros m.
destruct m.
+ reflexivity.
+ apply IHn.
Qed.
(** [] *)
(** **** Exercise: 3 stars, advanced, optional (eqb_sym_informal)
@@ -1184,12 +1345,36 @@ Proof.
Give an informal proof of this lemma that corresponds to your
formal proof above:
Theorem: For any [nat]s [n] [m], [(n =? m) = (m =? n)].
Theorem: For any [nat]s [n] [m], [(n =? m) = (m =? n)].
Proof: *)
(* FILL IN HERE
Proof: by induction on n.
[] *)
First consider the base case where n = 0.
If m = 0, then
(n ?= m) = (0 ?= 0) = true = (m ?= n).
If m = S m' for some natural number m', then
(n ? m) = (0 ?= S m') = false = (S m' ?= true)
Now consider the inductive case where n = S n' for some natural number n'.
We have the following induction hypothesis:
forall m, (n' ?= m) = (m ?= n').
Let's consider the case where m = 0. Then
(n ?= m) = (S n' ?= 0) = false = (0 ?= S n').
Now consider the case where m = S m' for some natural number m'.
We now need to show that:
(S n' =? S m) = (S m =? S n')
Which is immediate from the induction hypothesis. Qed.
*)
(** **** Exercise: 3 stars, standard, optional (eqb_trans) *)
Theorem eqb_trans : forall n m p,
@@ -1197,7 +1382,12 @@ Theorem eqb_trans : forall n m p,
m =? p = true ->
n =? p = true.
Proof.
(* FILL IN HERE *) Admitted.
intros n m p Hnm Hmp.
apply eqb_true in Hnm.
apply eqb_true in Hmp.
subst.
apply eqb_refl.
Qed.
(** [] *)
(** **** Exercise: 3 stars, advanced (split_combine)
@@ -1211,14 +1401,38 @@ Proof.
Your property will need to account for the behavior of [combine]
in its base cases, which possibly drop some list elements. *)
Definition split_combine_statement : Prop
(* ("[: Prop]" means that we are giving a name to a
logical proposition here.) *)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition split_combine_statement : Prop :=
forall (X Y : Type) (l : list (X * Y)) (l1 : list X) (l2 : list Y),
length l1 = length l2 ->
combine l1 l2 = l ->
split l = (l1, l2).
Theorem split_combine : split_combine_statement.
Proof.
(* FILL IN HERE *) Admitted.
unfold split_combine_statement.
intros X Y l.
induction l as [| [x y] t IH].
- intros l1 l2 Hlen Hcombine.
destruct l1 as [| x1 t1] eqn:Hl1.
+ destruct l2 as [| y1 t2] eqn:Hl2.
* simpl. reflexivity.
* discriminate.
+ destruct l2 as [| y1 t2] eqn:Hl2.
* discriminate.
* discriminate.
- intros l1 l2 Hlen Hcombine.
destruct l1 as [| x1 t1] eqn:Hl1.
+ discriminate.
+ destruct l2 as [| y1 t2] eqn:Hl2.
* discriminate.
* injection Hlen as Hlen'.
injection Hcombine as Hcombine'.
specialize (IH t1 t2 Hlen' H0).
subst.
simpl.
rewrite IH.
reflexivity.
Qed.
(* Do not modify the following line: *)
Definition manual_grade_for_split_combine : option (nat*string) := None.
@@ -1230,7 +1444,24 @@ Theorem filter_exercise : forall (X : Type) (test : X -> bool)
filter test l = x :: lf ->
test x = true.
Proof.
(* FILL IN HERE *) Admitted.
intros X test x l lf H.
generalize dependent x.
induction l as [| x' xs IHf].
- intros x H.
simpl in H.
discriminate H.
- intros x H.
destruct (test x') eqn:Htst.
+ unfold filter in H.
rewrite Htst in H.
injection H as Hx Htail.
rewrite Hx in Htst.
apply Htst.
+ apply IHf.
unfold filter in H.
rewrite Htst in H.
apply H.
Qed.
(** [] *)
(** **** Exercise: 4 stars, advanced, especially useful (forall_exists_challenge)
@@ -1259,43 +1490,63 @@ Proof.
[existsb'] and [existsb] have the same behavior.
*)
Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool :=
match l with
| nil => true
| x :: xs => test x && forallb test xs
end.
Example test_forallb_1 : forallb odd [1;3;5;7;9] = true.
Proof. (* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_forallb_2 : forallb negb [false;false] = true.
Proof. (* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_forallb_3 : forallb even [0;2;4;5] = false.
Proof. (* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_forallb_4 : forallb (eqb 5) [] = true.
Proof. (* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Fixpoint existsb {X : Type} (test : X -> bool) (l : list X) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Fixpoint existsb {X : Type} (test : X -> bool) (l : list X) : bool :=
match l with
| nil => false
| x :: xs => test x || existsb test xs
end.
Example test_existsb_1 : existsb (eqb 5) [0;2;3;6] = false.
Proof. (* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_existsb_2 : existsb (andb true) [true;true;false] = true.
Proof. (* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_existsb_3 : existsb odd [1;0;0;0;0;3] = true.
Proof. (* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_existsb_4 : existsb even [] = false.
Proof. (* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Definition existsb' {X : Type} (test : X -> bool) (l : list X) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(* NOTE: A || B || ... is equivalent to ~(~A && ~B && ...) *)
Definition existsb' {X : Type} (test : X -> bool) (l : list X) : bool :=
negb (forallb (fun x => negb (test x)) l).
Theorem existsb_existsb' : forall (X : Type) (test : X -> bool) (l : list X),
existsb test l = existsb' test l.
Proof. (* FILL IN HERE *) Admitted.
Proof.
intros X test l.
induction l as [| b bs IHt].
- reflexivity.
- simpl.
unfold existsb'.
destruct (test b) eqn:Htst.
+ simpl.
rewrite Htst.
reflexivity.
+ simpl.
rewrite Htst.
simpl.
apply IHt.
Qed.
(** [] *)
(* 2026-01-07 13:17 *)