Hi folks! I'm a new user working through logical foundations. I've previously read "the little typer" and i'm loving my experience so far! However, I'm currently stuck on one of the extra exercises in chapter 2 (induction). specifically on proving mult_assoc
.
I've gotten this far, but i'm failing to come up with anything clever for the inductive case:
Theorem mult_assoc : forall n m p : nat,
n * (m * p) = (n * m) * p.
Proof.
intros n m p.
induction n as [n' IHn'].
 simpl.
reflexivity.

any hints?
i've tried nested induction on m and also destructing p. i think i've actually done both nested :) feels like i'm missing something more straight forward
Start with simpl
again.
yes, this is the route i went before. after applying my inductive rewrite, i end up here:
1 subgoal
n', m, p : nat
IHn' : n' * (m * p) = n' * m * p
========================= (1 / 1)
m * p + n' * m * p = (m + n' * m) * p
Theorem mult_assoc : forall n m p : nat,
n * (m * p) = (n * m) * p.
Proof.
intros n m p.
induction n as [n' IHn'].
 simpl.
reflexivity.
 simpl.
rewrite > IHn'.
i feel close! seems like i need some kind of assoc rule for addition or possibly an assert
last night i tried inducting or destructing again at this point, but i feel i'm missing something more obvious.
I think you should Search
for a lemma about times and plus, and use that.
What you see is the distributivity of multiplication over addition, you need to either use a stdlib lemma for that, or prove it yourself separately.
thanks! these are very helpful tips. much appreciated!
i've proven this earlier in the chapter:
Theorem mult_plus_distr_r : forall n m p : nat,
(n + m) * p = (n * p) + (m * p).
Proof.
intros n m p.
induction n as [n' IHn'].
 simpl.
rewrite > mul_comm.
reflexivity.
 induction m as [m' IHm'].
+ simpl.
rewrite > add_0_r.
rewrite > add_0_r.
reflexivity.
+ simpl.
rewrite > IHn'.
simpl.
rewrite > add_assoc.
reflexivity.
Qed.
don't judge my repetitive rewrites! they feel suboptimal.
ha, that worked perfectly! thanks for the rubber ducking :)
Theorem mult_assoc : forall n m p : nat,
n * (m * p) = (n * m) * p.
Proof.
intros n m p.
induction n as [n' IHn'].
 simpl.
reflexivity.
 simpl.
rewrite > IHn'.
rewrite > mult_plus_distr_r.
reflexivity.
Qed.
unrelated, but wow is coqtail nice. i'm impressed with the tooling as a new user.
Enrico Tassi has marked this topic as resolved.
I'm a bit farther on and trying to prove :
Theorem plus_n_n_injective : forall n m,
n + n = m + m >
n = m.
Proof.
intros n.
induction n as [n' IHn'].
 intros m.
destruct m as [m'] eqn:E.
+ reflexivity.
+ discriminate.
 intros m.
destruct m as [m'] eqn:E.
+ discriminate.
+ intro H.
f_equal.
simpl in H.
rewrite < plus_n_Sm in H.
rewrite < plus_n_Sm in H.
here's data about my current goal:
1 subgoal
n' : nat
IHn' : forall m : nat, n' + n' = m + m > n' = m
m, m' : nat
E : m = S m'
H : S (S (n' + n')) = S (S (m' + m'))
========================= (1 / 1)
n' = m'
i'd like to apply the following lemma in H
: eq_add_S: forall n m : nat, S n = S m > n = m
but doing so causes an error:
rewrite > eq_add_S in H.
produces: Unable to find an instance for the variable m.
am i totally on the wrong track?
What about apply "eq_add_S in H"?
you want apply in
not rewrite in
can you all help me with a more colloquial understanding of apply in the context? is it backwards implication or forwards?
phew, thanks to everyone!
Theorem plus_n_n_injective : forall n m,
n + n = m + m >
n = m.
Proof.
intros n.
induction n as [n' IHn'].
 intros m.
destruct m as [m'] eqn:E.
+ reflexivity.
+ discriminate.
 intros m.
destruct m as [m'] eqn:E.
+ discriminate.
+ intro H.
f_equal.
simpl in H.
rewrite < plus_n_Sm in H.
rewrite < plus_n_Sm in H.
apply eq_add_S in H.
apply eq_add_S in H.
apply IHn' in H.
apply H.
Qed.
i still don't feel i have a good intuitive understanding of apply vs rewrite
specifically, rewrite >
feels identical to apply
in H
here.
@drew apply lemma in H
replaces H
by lemma … H
(where …
are inferred arguments.)
ah, so apply infers the polymorphic arguments where rewrite does not?
sorry, both infer them; no difference.
but I might know what you mean.
i guess i'm struggling with how rewrite > lemma in H
and apply lemma in H
differ here
my naive understanding of apply lemma
was basically reflexivity . rewrite > lemma
given lemma : foo <> bar
, you can use _both_ rewrite > lemma in H
and apply lemma in H
.
with the same result.
but if lemma : foo > bar
, rewrite lemma
will _not_ replace foo
by bar
— basically under any circumstance
i see. i haven't arrived at <>
yet :)
this is bidirectional implication?
yes
awesome, thanks for the thoughtful responses. very helpful!
instead, rewrite
will fall back to its usual “let’s look for an equality” strategy; for eq_add_S: forall n m : nat, S n = S m > n = m
, it’ll find n = m
, and try to rewrite n
with m
.
ah, hence the no m
error
which will fail because n
could be anything!
yeah, I’m confused why it complains on m
instead of n
, but I’ve learned to not ask _those_ questions
lol
i'm glad it's not just me
an apply in
is forwards implication whereas apply
on a goal is backwards implication?
i think i get it!
hey, at least i was close and on the right track
yeah you’re doing good :)
and asking good questions
it turns out that learning how to use Coq Search is also very helpful
good error messages are _really hard_, doing those for Coq is even harder, and Coq doesn’t have the resources of something like Rust (which has some of the best error messages around)
totally understood. my first venture into dependent types and automated proofs was via "the little typer"
which i feel prepared me with the fundamentals very well for this material
i'd be totally lost otherwise
rewrite sees that you want to rewrite n into m, so it looks to see what matches n
in the term to rewrite (the type of H)
in this case that means it picks the first subterm with the right type
then it sees that this isn't enough to constrain m
, so it complains about m
is another way to think about rewrite that if used with an implication, it totally ignores the left side of >
?
it's operating on the equality, not the implication itself?
sorry, totally ignores the left side, editing
(deleted)
if you want to you can provide a m: rewrite IHn' with (m:=0) in H .
(this is a nonsense rewrite of course)
the left side of the arrow produces a sidecondition goal
ha, got it. i'm doing a lot of experimenting with the tactics forms as the book introduces them
@Gaëtan Gilbert ah thanks. I was confused because the other rewrite tactic (from ssreflect) wouldn’t even try to instantiate n
in this case, or at least so I thought…
with ssreflect I get Error: Unable to find an instance for the variable m.
Rule's type: (forall m : nat, n' + n' = m + m > n' = m)
(on rewrite IHn' in H .
)
in this case rewrite IHn' in H
won't lead to anything interesting, but if you really want to use rewrite you could do
rewrite IHn' with (m:=m').
* reflexivity.
* assumption.
another question  when operating on the goal, how does f_equal
differ from apply f_equal
?
it mostly doesn't, except for borderline differences like doing nothing instead of an error if the goal doesn't have the right shape (eg Goal bool. f_equal.
has no error and no effect)
and handling functions with more than 1 argument, eg a goal x + y = a + b
will produce subgoals x = a
and y = b
with the tactic and error with the apply
well this conversation _definitely_ helped, i just proved this using similar techniques in about a minute
Theorem nth_error_after_last: forall (n : nat) (X : Type) (l : list X),
length l = n >
nth_error l n = None.
Proof.
intros n X l.
generalize dependent n.
induction l as [x l' IHl'].
 intros n.
simpl. reflexivity.
 intros n.
simpl.
destruct n as [n'].
+ discriminate.
+ intros H.
apply eq_add_S in H.
apply IHl'.
apply H.
Qed.
why length l = n
instead of length l <= n
?
don't ask me, i'm just proving what the book gives me
i'm working through the tactics section that introduces unfold
and i'm struggling with the combine_split
exercise. here's what i have so far:
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) >
combine l1 l2 = l.
Proof.
intros X Y l l1 l2.
induction l as [xy l' IHl'].
 intros H.
destruct l1 as [x l1'] eqn:E.
+ reflexivity.
+ injection H as H1 H2.
rewrite < H2.
reflexivity.
 intros H.
1 subgoal
X : Type
Y : Type
xy : X * Y
l' : list (X * Y)
l1 : list X
l2 : list Y
IHl' : split l' = (l1, l2) > combine l1 l2 = l'
H : split (xy :: l') = (l1, l2)
========================= (1 / 1)
combine l1 l2 = xy :: l'
clearly i need to use unfold
somewhere, but doing so seems to just make things more complicated
Gaëtan Gilbert has marked this topic as unresolved.
if you mean https://deepspec.github.io/sf/lfcurrent/Tactics.html#lab157 that's not in the unfold chapter (maybe you didn't notice the "Using destruct on Compound Expressions" chapter heading?)
i'm still struggling with this. current state:
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) >
combine l1 l2 = l.
Proof.
intros X Y l l1 l2.
induction l as [xy l' IHl'].
+ simpl.
intros H.
injection H as H1 H2.
rewrite < H1.
rewrite < H2.
reflexivity.
+
1 subgoal
X : Type
Y : Type
xy : X * Y
l' : list (X * Y)
l1 : list X
l2 : list Y
IHl' : split l' = (l1, l2) > combine l1 l2 = l'
========================= (1 / 1)
split (xy :: l') = (l1, l2) > combine l1 l2 = xy :: l'
IHl'
doesn't seem to help me at all here.
like there's no way l' = xy :: l'
, so i'm not sure what i can do
i'm struggling to understand a compound expression i can destruct on to help this
perhaps i need to do some destructing before my induction
Hum, maybe try not introducing all variables before doing induction.
i get to what feels like a similar spot:
1 subgoal
X : Type
Y : Type
xy : X * Y
l' : list (X * Y)
IHl' : forall (l1 : list X) (l2 : list Y),
split l' = (l1, l2) > combine l1 l2 = l'
========================= (1 / 1)
forall (l1 : list X) (l2 : list Y),
split (xy :: l') = (l1, l2) > combine l1 l2 = xy :: l'
though i understand that IHl'
is more useful as it works for _any_ l1
and l2
i'm struggling to see how i can employ destructing on compound expressions here
Forget about destructing; there's work to do first, like in the other branch, such as simpl
Crucially, simpl
will progress on split (xy :: l')
, and give you a more exciting goal.
(but destruct
will not come so late I suspect)
Indeed in order to prove anything about a recursive program like split
you have to evaluate it a little. Induction gave you some gas, namely ::
, so the program should make some progress.
more in general, a strategy that often works on these proofs is to “follow the computation” — in this case, of split
: you mirror the pattern matches and recursion of that function in your proof.
e
? Use destruct e
— or destruct e eqn:Hname
… but if we recurse on a piece, use induction instead. Often start topdown.Until now, we see:
split
does a pattern match and recursion on its input? We’ll need induction on it — and then simpl
.split
does nested matches, on xy
and on split l’
: we _might_ need to use destruct
on those.of course this strategy, “follow your nose through computation”, doesn’t always work, and you must choose when which computation to follow, but this strategy is often a solid starting point AFAICT (I wonder if somebody ever described it properly).
Isn’t that more or less what functional induction does? Or the funelim
tactic from Equations?
indeed relevant, but I wouldn’t use either for Logical Foundations :wink: .
Sure! I only meant to say that this strategy has been at least automated, if not described ;)
thanks everyone! will take another shot today.
so, i've gotten this far:
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) >
combine l1 l2 = l.
Proof.
intros X Y l.
induction l as [xy l' IHl'].
+ simpl.
intros l1 l2 H.
injection H as H1 H2.
rewrite < H1.
reflexivity.
+ intros l1 l2.
simpl.
1 subgoal
X : Type
Y : Type
xy : X * Y
l' : list (X * Y)
IHl' : forall (l1 : list X) (l2 : list Y),
split l' = (l1, l2) > combine l1 l2 = l'
l1 : list X
l2 : list Y
========================= (1 / 1)
match xy with
 (x, y) => match split l' with
 (lx, ly) => (x :: lx, y :: ly)
end
end = (l1, l2) > combine l1 l2 = xy :: l'
what i'm struggling with is that IHl'
deals with the specific l'
that i have from the induction
if i add destruct xy as [x' y'].
i get:
match split l' with
 (lx, ly) => (x' :: lx, y' :: ly)
end = (l1, l2) > combine l1 l2 = (x', y') :: l
as my goal
which seems maybe closer?
It's alright that IHl'
talks about l'
because split l'
is also in the goal.
l1
and l2
are really determined by l'
. You can destruct (split l') eqn:Hsplit
to simplify the equation, without losing information (recorded in Hsplit
).
oof, i got it, but i'm not sure it is ideal.
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) >
combine l1 l2 = l.
Proof.
intros X Y l.
induction l as [xy l' IHl'].
+ simpl.
intros l1 l2 H.
injection H as H1 H2.
rewrite < H1.
reflexivity.
+ simpl.
destruct (split l') as [xs ys] eqn:Hsplit.
destruct xy as [x y] eqn:XY.
intros l1 l2 H.
injection H as H1 H2.
rewrite < H1.
rewrite < H2.
simpl.
f_equal.
apply IHl'.
reflexivity.
Qed.
you don’t need eqn:XY
, but otherwise this looks reasonable.
hsplit doesn't look used either
Ah! Doing simpl first avoids the need for it.
To see the point of the exercise, it might be worthwhile to do both destruct... eqn first, then simpl, then continue. The result is a strictly worse proof, but "do simpl first" only works sometimes, while eqn: works always
re the unused eqn
lines, i’m following the author’s suggestion to always include them for now.
once i understand the rules i will start breaking them :grinning:
I'm working on this current subgoal:
1 subgoal
(1 unfocused at this level)
X : Type
test : X > bool
x, lh : X
l' : list X
IHl' : forall lf : list X, [ ] = x :: lf > test x = true
lf : list X
========================= (1 / 1)
[lh] = x :: lf > test x = true
it looks to me like i should be able to rewrite < IHl'
but if i attempt to do so, I get:
Unable to find an instance for the variable lf.
this is confusing to me because IHl'
seems that it should work for _all_ lf
i guess maybe i have to intros H
i'm also surprised i can't use discriminate on lf = x :: lf
hey, i did it!
Theorem filter_exercise : forall (X : Type) (test : X > bool)
(x : X) (l lf : list X),
filter test l = x :: lf >
test x = true.
Proof.
intros X test x l lf.
induction l as [lh l' IHl'].
+ simpl. discriminate.
+ simpl.
destruct (test lh) eqn:Htest.
++ intros H.
injection H as H1 H2.
rewrite < H1.
rewrite > Htest.
reflexivity.
++ apply IHl'.
Qed.
drew said:
this is confusing to me because
IHl'
seems that it should work for _all_lf
Indeed it works for any lf : list X
but you still need to show that there exists at least one such lf : list X
in your context. You could rewrite < (IHl' lf)
@Kenji Maillard thanks. i was looking for an example of "applying" an generalized hypothesis. this helps.
it turns out introducing lf earlier helped out here as well, which makes sense
drew said:
i'm also surprised i can't use discriminate on
lf = x :: lf
Actually, proving that lf = x :: lf > False
requires a proof by induction so it's not entirely trivial (for instance it wouldn't hold for a coinductive type of infinite lists/streams)
@Kenji Maillard True but confusing for many — nonexperts would benefit from having a warning, or a variant of discriminate that would do the induction automatically on inductives…
@Paolo Giarrusso I fully agree that discharging such goals easily would be something useful for nonexperts, but It should probably be a tactic distinct from discriminate
, and I'm not sure how to specify its behaviour. Maybe something along the lines "solves any goal by extracting two terms u, v such that u is a strict subterm of v and C[u] = C[v] with C[] an injective context" using the notion of subterm derived by Equations (or maybe Elpi)...
What about the “occurs check” from unification?
sorry, you did say “strict subterm” :sweat_smile:
I forget if congruence
does this, but I thought it was meant to be complete for some theory. How do we extend that theory to understand inductives? Such a theory can already derive C[u] = C[v] ==> u = v.
i'm back! i'm working though the logic chapter and _close_ on this exercise:
Theorem In_map_iff :
forall (A B : Type) (f : A > B) (l : list A) (y : B),
In y (map f l) <>
exists x, f x = y /\ In x l.
Proof.
intros A B f l y.
split.
 induction l as [a l' IHl'].
+ simpl. intros [].
+ simpl. intros [H  H].
++ exists a. split.
+++ apply H.
+++ left. reflexivity.
++ apply IHl' in H.
destruct H as [x H].
exists x.
split.
+++ destruct H as [H _]. apply H.
+++ destruct H as [_ H]. right. apply H.
 induction l as [a l' IHl'].
+ simpl.
intros [x H].
simpl in H.
destruct H as [_ H].
destruct H.
+ intros [x H].
simpl.
1 subgoal
A : Type
B : Type
f : A > B
a : A
l' : list A
y : B
IHl' : (exists x : A, f x = y /\ In x l') > In y (map f l')
x : A
H : f x = y /\ In x (a :: l')
========================= (1 / 1)
f a = y \/ In y (map f l')
i've tried:
right.
apply IHl'.
exists x.
which gets me to:
1 subgoal
A : Type
B : Type
f : A > B
a : A
l' : list A
y : B
IHl' : (exists x : A, f x = y /\ In x l') > In y (map f l')
x : A
H : f x = y /\ In x (a :: l')
========================= (1 / 1)
f x = y /\ In x l'
but i'm not sure how to deal with the fact that my H
has a :: l'
inside of it
i'd also love to just be able to do left
but my f a = y
is bound to a
whereas my H
is bound to x
:
Theorem In_map_iff :
forall (A B : Type) (f : A > B) (l : list A) (y : B),
In y (map f l) <>
exists x, f x = y /\ In x l.
Proof.
intros A B f l y.
split.
 induction l as [a l' IHl'].
+ simpl. intros [].
+ simpl. intros [H  H].
++ exists a. split.
+++ apply H.
+++ left. reflexivity.
++ apply IHl' in H.
destruct H as [x H].
exists x.
split.
+++ destruct H as [H _]. apply H.
+++ destruct H as [_ H]. right. apply H.
 induction l as [a l' IHl'].
+ simpl.
intros [x H].
simpl in H.
destruct H as [_ H].
destruct H.
+ intros [x H].
simpl.
right.
apply IHl'.
exists x.
split.
++ destruct H as [H1 H2].
apply H1.
++
H : f x = y /\ In x (a :: l')
this allows for x = a
in which case you need to go left
in other words you went tight too early
1 subgoal
A : Type
B : Type
f : A > B
a : A
l' : list A
y : B
IHl' : (exists x : A, f x = y /\ In x l') > In y (map f l')
x : A
H : f x = y /\ In x (a :: l')
========================= (1 / 1)
In x l'
that's going further down the current path
go back to before you did right
and do simpl in H
AH, yes!
that makes sense.
phew!
Proof.
intros A B f l y.
split.
 induction l as [a l' IHl'].
+ simpl. intros [].
+ simpl. intros [H  H].
++ exists a. split.
+++ apply H.
+++ left. reflexivity.
++ apply IHl' in H.
destruct H as [x H].
exists x.
split.
+++ destruct H as [H _]. apply H.
+++ destruct H as [_ H]. right. apply H.
 induction l as [a l' IHl'].
+ simpl.
intros [x H].
simpl in H.
destruct H as [_ H].
destruct H.
+ intros [x H].
simpl.
simpl in H.
destruct H as [H1 H2].
destruct H2 as [H2  H2].
++ left. rewrite > H2. apply H1.
++ right.
apply IHl'.
exists x.
split.
+++ apply H1.
+++ apply H2.
Qed.
it feels like i overcomplicated this one
is there a way to go to from H1
and H2
in context to H1 /\ H2
in context?
that would simplify the last leg, at least
destruct H as [H1 H2].
destruct H2 as [H2  H2].
you can combine this as destruct H as [H1 [H2  H2]]
split.
+++ apply H1.
+++ apply H2.
or split; assumption
or exact (conj H1 H2)
btw I see you go 
+
++
+++
with bullets, but I think usually people use *
after +
thanks!
but i'm not missing anything fundamental in these proofs so far? i appreciate all the feedback.
i'm not sure where to go from here:
Theorem tr_rev_correct : forall X, @tr_rev X = @rev X.
Proof.
intros X.
apply functional_extensionality.
unfold tr_rev.
intros l.
induction l as [x l' IHl].
 reflexivity.
 simpl.
rewrite < IHl.
1 subgoal
X : Type
x : X
l' : list X
IHl : rev_append l' [ ] = rev l'
========================= (1 / 1)
rev_append l' [x] = rev_append l' [ ] ++ [x]
unfold
ing rev_append
doesn't seem to do much for me
you'll need to make some sort of lemma
consider how you would prove the theorem in a non formal way
yes, i tried extracting a lemma saying exactly rev_append l' [x] = rev_append l' [ ] ++ [x]
but then i struggled to solve that, for the same reason i'm struggling at this point :)
basically i'm stuck here with a similar problem:
Lemma rev_append_singleton : forall X (x : X) (l : list X),
rev_append l [x] = rev_append l [ ] ++ [x].
Proof.
intros X x l.
induction l as [x' l' IHl'].
 reflexivity.

hmm wait, maybe i'm not!
well i'm getting closer anyway
Lemma rev_app_dist : forall X (l l1 l2 : list X),
rev_append l (l1 ++ l2) = rev_append l l1 ++ l2.
Proof.
intros X l.
induction l as [x' l' IHl'].
 reflexivity.
 simpl.
Theorem tr_rev_correct : forall X, @tr_rev X = @rev X.
Proof.
intros X.
apply functional_extensionality.
unfold tr_rev.
intros l.
induction l as [x l' IHl].
 reflexivity.
 simpl.
rewrite < IHl.
rewrite < rev_app_dist.
reflexivity.
Qed.
but i'm stuck in a sort of similar spot
1 subgoal
X : Type
x' : X
l' : list X
IHl' : forall l1 l2 : list X,
rev_append l' (l1 ++ l2) = rev_append l' l1 ++ l2
========================= (1 / 1)
forall l1 l2 : list X,
rev_append l' (x' :: l1 ++ l2) = rev_append l' (x' :: l1) ++ l2
that's a weird lemma to try to prove
instead I would try to characterize rev_append l1 l2
for any l1 and l2 (ie prove a lemma with statement forall l1 l2, rev_append l1 l2 = something
)
(note you should be able to prove that goal, it's just not the nicest statement)
hey i proved my gross lemma!
Lemma rev_app_dist : forall X (l l1 l2 : list X),
rev_append l (l1 ++ l2) = rev_append l l1 ++ l2.
Proof.
intros X l.
induction l as [x' l' IHl'].
 reflexivity.
 intros l1 l2.
simpl.
rewrite < (IHl' (x' :: l1) l2).
reflexivity.
Qed.
Theorem tr_rev_correct : forall X, @tr_rev X = @rev X.
Proof.
intros X.
apply functional_extensionality.
unfold tr_rev.
intros l.
induction l as [x l' IHl].
 reflexivity.
 simpl.
rewrite < IHl.
rewrite < rev_app_dist.
reflexivity.
Qed.
i'll take a pass it at your lemma a bit later, thanks for the tips!
ok i'm going bonkers with this "simple" 1 star exercise:
Theorem eqb_neq : forall x y : nat,
x =? y = false <> x <> y.
Proof.
intros x y.
rewrite < (not_true_is_false (x =? y)).
2 subgoals
x, y : nat
========================= (1 / 2)
(x =? y) = (x =? y) <> x <> y
========================= (2 / 2)
(x =? y) <> true
i must be missing something fundamental because i don't see how to progress on these subgoals
one of my ideas was:
Theorem eqb_neq : forall x y : nat,
x =? y = false <> x <> y.
Proof.
intros x y.
rewrite < (not_true_is_false (x =? y)).
 split.
+ destruct (x =? y).
but, uh,:
2 subgoals
(1 unfocused at this level)
x, y : nat
========================= (1 / 2)
true = true > x <> y
========================= (2 / 2)
false = false > x <> y
the hint says not_true_iff_false
(iff
not is
)
well hey, that helps :)
Theorem eqb_neq : forall x y : nat,
x =? y = false <> x <> y.
Proof.
intros x y. rewrite < (not_true_iff_false (x =? y)). split.
 intros H1 H2. unfold not in H1. apply H1. rewrite > H2. apply eqb_refl.
 unfold not. intros H1 H2. apply eqb_true in H2. apply H1. apply H2.
Qed.
ok that did _not_ feel like one star
i swear some of the 4 star exercises feel straight forward and some 12 star feel very challenging. perhaps it is related to my background in traditional pure FP that makes some exercises easier.
i swear some of the 4 star exercises feel straight forward and some 12 star feel very challenging
we've all been there
ha, thanks :)
we've all been there
... maybe the ratings need some improvement? I didn't go through SF at all, but judging difficulty is notoriously difficult if you are already an expert. I think SF is / was used in some classroom settings, so there must already have been some rating adjustment over the years, but additional feedback would probably be well received, particularly if you have a list of problems whose ratings sound felt wrong to you. With enough people submitting such lists, things could converge to better ratings. But I have no idea if there is infrastructure permitting such a convergence, or more importantly if someone would like to put in the effort to build such an infrastructure.
that's a very good point. i'm working through this on my own (plus the very awesome help from this chat) and the only background i have before this is some complexity theory proofs in grad school and having read "the little typer"
so perhaps some things that are challenging for me would not be for folks going straight into phd programs
Sure, what's challenging for a person is not necessarily challenging for another, and the other way around. That's why this would need feedback from many people in order to work.
there have been "user studies" of theorem proving tasks that try to figure out what is hard or easy for most people, I think we summarized a few of them in our survey
general question  if i have a hypothesis a1 :: l1' = a2 :: l2'
how can i get a1 = a2 /\ l1' = l2'
. when this was in the goal, i was able to use f_equal
separately, i often find myself doing split. reflexivity. reflexivity.
or some such thing. is there are shortcut for "split and do the same operation on both resulting things"?
drew said:
general question  if i have a hypothesis
a1 :: l1' = a2 :: l2'
how can i geta1 = a2 /\ l1' = l2'
. when this was in the goal, i was able to usef_equal
injection H
drew said:
separately, i often find myself doing
split. reflexivity. reflexivity.
or some such thing. is there are shortcut for "split and do the same operation on both resulting things"?
split; reflexivity
ah, that ;
is sneaky, thanks!
is there a way for me to do the equivalent of injection H
without intros H
if my hypothesis is on the left side of a >
in the goal?
(thanks as always, very helpful)
intros [= H1 H2]
Is there any lemma for currying? I have this theorem:
Axiom functional_extensionality : forall {X Y: Type}
{f g : X > Y},
(forall (x:X), f x = g x) > f = g.
Fixpoint rev (X : Type) (l : list X) {struct l} : list X :=
match l with
 [ ] => [ ]
 h :: t => rev X t ++ [h]
end.
Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
match l1 with
 [] => l2
 x :: l1' => rev_append l1' (x :: l2)
end.
Definition tr_rev {X} (l : list X) : list X :=
rev_append l [].
Theorem tr_rev_correct : forall X, @tr_rev X = @rev X.
intro. apply functional_extensionality. unfold tr_rev.
intros. induction x as [x xs IHx]. reflexivity.
simpl. rewrite < IHx.
replace ([x]) with ([ ] ++ [x]) at 1 by reflexivity.
GOAL:
X : Type
x : X
xs : list X
IHx : rev_append xs [ ] = rev X xs
========================= (1 / 1)
rev_append xs ([ ] ++ [x]) = rev_append xs [ ] ++ [x]
It's just a matter of where the parenthesis are, is there any lemma on standard library to finish this goal?
It's a lemma about rev_append
you need, and since you defined it, you'll have to prove it.
Thanks @Liyao I will try to write some auxiliary lemmas on rev_append
hey all, i'm stuck on what seems like an obvious step in a proof.
i'm here:
Theorem ev_sum : forall n m, ev n > ev m > ev (n + m).
Proof.
intros n m En.
induction En as [n' En' IHn].
 simpl. intros Em. apply Em.
 simpl. intros Em.
with this following context:
1 subgoal
m, n' : nat
En' : ev n'
IHn : ev m > ev (n' + m)
Em : ev m
========================= (1 / 1)
ev (S (S (n' + m)))
i have evSS_ev
available to me, which seems like should "just work"
but applying it _adds_ S (S ..
rather than removing it
am i on the wrong track? my other idea was to use induction on Em or use inversion.
evSS_ev is:
Theorem evSS_ev : forall n,
ev (S (S n)) > ev n.
You need a lemma with ev (S (S _))
as a conclusion.
Like ev_SS
.
apply
matches the conclusion of the lemma with the conclusion in your goal.
wow, of course, i can use the constructor itself
thanks, that's a facepalm moment
all finished now:
Theorem ev_sum : forall n m, ev n > ev m > ev (n + m).
Proof.
intros n m En.
induction En as [n' En' IHn].
 simpl. intros Em. apply Em.
 simpl. intros Em. apply ev_SS. apply IHn. apply Em.
Qed.
BTW here I would intro Em before doing the induction
yes, good point
i feel like i've gotten used to late intros when initially exploring a proof via induction
late intro would need to revert m
here
Last updated: Sep 26 2023 at 13:01 UTC