I am working on the exercises in the List chapter of Software Foundation. I am working particularly on this exercise - “Adding a value to a bag should increase the value’s count by one. State that as a theorem and prove it.”
I am trying to figure out how to prove this theorem:
Blockquote
Theorem bag_theorem1 : forall (n : nat) (b:bag),
S (count n b) = count n (add n b).
I am able to solve the case “b=” with two lemmas as follows:
Blockquote
Lemma add_null: forall n, add n = [n].
Proof.
intros. destruct n.
simpl. reflexivity.
simpl. reflexivity.
Qed.
Blockquote
Lemma count_p: forall p, count p [p] = 1.
Proof.
intros p.
induction p as [|p’ IHp].
simpl. reflexivity.
simpl in IHp. simpl. assumption.
Qed.
Blockquote
Theorem bag_theorem1 : forall (n:nat) (b:bag),
S (count n b) = count n (add n b).
Proof.
intros n b.
induction b as [|x l IHb].
simpl. rewrite add_null. rewrite → count_p. reflexivity.
(how to solve the second case?)
However, I got stuck in the second case.
Thank you very much for your help!!
The answer may depend on how exactly you define add and count. However you are probably trying too much to rely on induction/destruct even when it is not necessary:
I would not be surprised if your lemma add_null could be proved by just reflexivity.,
and concerning bag_theorem1, starting by intros n b; simpl. might give you some hint on what you should do.
Thank you for your suggestions. I tried starting by intros n b; simpl but nothing has changed in the goal. Here are the definitions about add and count:
Definition add (v:nat) (s:bag) : bag :=
match v with
| O => O::s
| S v’ => (S v’)::s
end.
Fixpoint equal(a b:nat): bool:=
match a, b with
| O, O => true
| S a’, S b’ => equal a’ b’
| O, S b’ => false
| S a’, O => false
end.
Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil => O
| sh::st => match (equal sh v) with
| true => S (count v st)
| _ => count v st
end
end.
Let us focus on your definition of add: it starts with a match on v which explains why you need to destruct v each time you want to compute with add.
Then two possibilities for the intros n b; simpl. to show what may help you in bag_theorem1:
either keep your definition of add and use intros n b; destruct n as [|n]; simpl. in bag_theorem1 (to make add compute, thanks to the destruct)
or remark in the definition of add that what you do in both branches is exactly the same: x => x::s, meaning that the match is in fact not necessary, and you can simplify the definition of add.
! Thank you very much. I tried your two solutions. They both worked. It looks very easy, now. I do realise that I didn’t understand how to make functions compute very well before. By the way, I am still wondering whether there is an easier way to solve this subgoal:
1 subgoal
n : nat
b : bag
S (count n b) =
match equal n n with
| true => S (count n b)
| false => count n b
end
I tried to use simpl it didn’t work. So I used assert (equal n n = true) as H then it worked. So, it shows that to make equal n n compute, we have to do either destruct n or induction n. Right?
Indeed equal a b is really defined by induction on a and b so you need to work on them to derive most of the properties of equal. Here the statement forall n, equal n n = true is a natural one to prove and requires induction on n.
! Thank you very much. I tried your two solutions. They both worked. It looks very easy, now. I do realise that I didn’t understand how to make functions compute very well before. By the way, I am still wondering whether there is an easier way to solve this subgoal: