Stream: Coq users

Topic: logical foundations

drew (Oct 19 2021 at 13:50):

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.

drew (Oct 19 2021 at 13:50):

I've gotten this far, but i'm failing to come up with anything clever for the inductive case:

drew (Oct 19 2021 at 13:51):

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.
  -

drew (Oct 19 2021 at 13:51):

any hints?

drew (Oct 19 2021 at 13:52):

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

Alexander Gryzlov (Oct 19 2021 at 14:04):

Start with simpl again.

drew (Oct 19 2021 at 14:06):

yes, this is the route i went before. after applying my inductive rewrite, i end up here:

drew (Oct 19 2021 at 14:06):

1 subgoal

n', m, p : nat
IHn' : n' * (m * p) = n' * m * p

========================= (1 / 1)

m * p + n' * m * p = (m + n' * m) * p

drew (Oct 19 2021 at 14:07):

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'.

drew (Oct 19 2021 at 14:07):

i feel close! seems like i need some kind of assoc rule for addition or possibly an assert

drew (Oct 19 2021 at 14:09):

last night i tried inducting or destructing again at this point, but i feel i'm missing something more obvious.

Enrico Tassi (Oct 19 2021 at 14:11):

I think you should Search for a lemma about times and plus, and use that.

Alexander Gryzlov (Oct 19 2021 at 14:11):

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.

drew (Oct 19 2021 at 14:12):

thanks! these are very helpful tips. much appreciated!

drew (Oct 19 2021 at 14:13):

i've proven this earlier in the chapter:

drew (Oct 19 2021 at 14:13):

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.

drew (Oct 19 2021 at 14:13):

don't judge my repetitive rewrites! they feel sub-optimal.

drew (Oct 19 2021 at 14:14):

ha, that worked perfectly! thanks for the rubber ducking :)

drew (Oct 19 2021 at 14:14):

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.

drew (Oct 19 2021 at 14:17):

unrelated, but wow is coqtail nice. i'm impressed with the tooling as a new user.

Notification Bot (Oct 19 2021 at 14:20):

Enrico Tassi has marked this topic as resolved.

drew (Oct 21 2021 at 13:28):

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.

drew (Oct 21 2021 at 13:28):

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'

drew (Oct 21 2021 at 13:29):

i'd like to apply the following lemma in H: eq_add_S: forall n m : nat, S n = S m -> n = m

drew (Oct 21 2021 at 13:29):

but doing so causes an error:

drew (Oct 21 2021 at 13:30):

rewrite -> eq_add_S in H. produces: Unable to find an instance for the variable m.

drew (Oct 21 2021 at 13:30):

am i totally on the wrong track?

Paolo Giarrusso (Oct 21 2021 at 13:30):

What about apply "eq_add_S in H"?

Gaëtan Gilbert (Oct 21 2021 at 13:30):

you want apply in not rewrite in

drew (Oct 21 2021 at 13:34):

can you all help me with a more colloquial understanding of apply in the context? is it backwards implication or forwards?

drew (Oct 21 2021 at 13:36):

phew, thanks to everyone!

drew (Oct 21 2021 at 13:36):

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.

drew (Oct 21 2021 at 13:36):

i still don't feel i have a good intuitive understanding of apply vs rewrite

drew (Oct 21 2021 at 13:38):

specifically, rewrite -> feels identical to apply in H here.

Paolo Giarrusso (Oct 21 2021 at 13:38):

@drew apply lemma in H replaces H by lemma … H (where … are inferred arguments.)

drew (Oct 21 2021 at 13:38):

ah, so apply infers the polymorphic arguments where rewrite does not?

Paolo Giarrusso (Oct 21 2021 at 13:39):

sorry, both infer them; no difference.

Paolo Giarrusso (Oct 21 2021 at 13:39):

but I might know what you mean.

drew (Oct 21 2021 at 13:39):

i guess i'm struggling with how rewrite -> lemma in H and apply lemma in H differ here

drew (Oct 21 2021 at 13:40):

my naive understanding of apply lemma was basically reflexivity . rewrite -> lemma

Paolo Giarrusso (Oct 21 2021 at 13:40):

given lemma : foo <-> bar, you can use _both_ rewrite -> lemma in H and apply lemma in H.

Paolo Giarrusso (Oct 21 2021 at 13:40):

with the same result.

Paolo Giarrusso (Oct 21 2021 at 13:41):

but if lemma : foo -> bar, rewrite lemma will _not_ replace foo by bar — basically under any circumstance

drew (Oct 21 2021 at 13:42):

i see. i haven't arrived at <-> yet :)

drew (Oct 21 2021 at 13:42):

this is bidirectional implication?

Paolo Giarrusso (Oct 21 2021 at 13:42):

yes

drew (Oct 21 2021 at 13:42):

awesome, thanks for the thoughtful responses. very helpful!

Paolo Giarrusso (Oct 21 2021 at 13:42):

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.

drew (Oct 21 2021 at 13:42):

ah, hence the no m error

Paolo Giarrusso (Oct 21 2021 at 13:42):

which will fail because n could be anything!

Paolo Giarrusso (Oct 21 2021 at 13:43):

yeah, I’m confused why it complains on m instead of n, but I’ve learned to not ask _those_ questions

drew (Oct 21 2021 at 13:43):

lol

drew (Oct 21 2021 at 13:43):

i'm glad it's not just me

drew (Oct 21 2021 at 13:43):

an apply in is forwards implication whereas apply on a goal is backwards implication?

drew (Oct 21 2021 at 13:44):

i think i get it!

drew (Oct 21 2021 at 13:44):

hey, at least i was close and on the right track

Paolo Giarrusso (Oct 21 2021 at 13:44):

yeah you’re doing good :-)

Paolo Giarrusso (Oct 21 2021 at 13:44):

and asking good questions

drew (Oct 21 2021 at 13:44):

it turns out that learning how to use Coq Search is also very helpful

Paolo Giarrusso (Oct 21 2021 at 13:44):

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)

drew (Oct 21 2021 at 13:45):

totally understood. my first venture into dependent types and automated proofs was via "the little typer"

drew (Oct 21 2021 at 13:45):

which i feel prepared me with the fundamentals very well for this material

drew (Oct 21 2021 at 13:45):

i'd be totally lost otherwise

Gaëtan Gilbert (Oct 21 2021 at 13:46):

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

drew (Oct 21 2021 at 13:47):

is another way to think about rewrite that if used with an implication, it totally ignores the left side of ->?

drew (Oct 21 2021 at 13:47):

it's operating on the equality, not the implication itself?

drew (Oct 21 2021 at 13:47):

sorry, totally ignores the left side, editing

Paolo Giarrusso (Oct 21 2021 at 13:47):

(deleted)

Gaëtan Gilbert (Oct 21 2021 at 13:47):

if you want to you can provide a m: rewrite IHn' with (m:=0) in H . (this is a nonsense rewrite of course)

Gaëtan Gilbert (Oct 21 2021 at 13:48):

the left side of the arrow produces a side-condition goal

drew (Oct 21 2021 at 13:48):

ha, got it. i'm doing a lot of experimenting with the tactics forms as the book introduces them

Paolo Giarrusso (Oct 21 2021 at 13:48):

@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…

Gaëtan Gilbert (Oct 21 2021 at 13:50):

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 .)

Gaëtan Gilbert (Oct 21 2021 at 13:53):

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.

drew (Oct 21 2021 at 13:54):

another question -- when operating on the goal, how does f_equal differ from apply f_equal?

Gaëtan Gilbert (Oct 21 2021 at 13:56):

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)

Gaëtan Gilbert (Oct 21 2021 at 13:58):

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

drew (Oct 21 2021 at 14:03):

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.

Gaëtan Gilbert (Oct 21 2021 at 14:04):

why length l = n instead of length l <= n?

drew (Oct 21 2021 at 14:04):

don't ask me, i'm just proving what the book gives me

drew (Oct 25 2021 at 14:08):

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:

drew (Oct 25 2021 at 14:08):

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.

drew (Oct 25 2021 at 14:08):

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'

drew (Oct 25 2021 at 14:09):

clearly i need to use unfold somewhere, but doing so seems to just make things more complicated

Notification Bot (Oct 25 2021 at 14:17):

Gaëtan Gilbert has marked this topic as unresolved.

Gaëtan Gilbert (Oct 25 2021 at 14:22):

if you mean https://deepspec.github.io/sf/lf-current/Tactics.html#lab157 that's not in the unfold chapter (maybe you didn't notice the "Using destruct on Compound Expressions" chapter heading?)

drew (Oct 25 2021 at 19:32):

i'm still struggling with this. current state:

drew (Oct 25 2021 at 19:32):

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.
  +

drew (Oct 25 2021 at 19:32):

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'

drew (Oct 25 2021 at 19:32):

IHl' doesn't seem to help me at all here.

drew (Oct 25 2021 at 19:33):

like there's no way l' = xy :: l', so i'm not sure what i can do

drew (Oct 25 2021 at 19:34):

i'm struggling to understand a compound expression i can destruct on to help this

drew (Oct 25 2021 at 19:34):

perhaps i need to do some destructing before my induction

Enrico Tassi (Oct 25 2021 at 19:39):

Hum, maybe try not introducing all variables before doing induction.

drew (Oct 25 2021 at 19:43):

i get to what feels like a similar spot:

drew (Oct 25 2021 at 19:43):

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'

drew (Oct 25 2021 at 19:59):

though i understand that IHl' is more useful as it works for _any_ l1 and l2

drew (Oct 25 2021 at 19:59):

i'm struggling to see how i can employ destructing on compound expressions here

Paolo Giarrusso (Oct 26 2021 at 07:28):

Forget about destructing; there's work to do first, like in the other branch, such as simpl

Paolo Giarrusso (Oct 26 2021 at 07:30):

Crucially, simpl will progress on split (xy :: l'), and give you a more exciting goal.

Paolo Giarrusso (Oct 26 2021 at 07:40):

(but destruct will not come so late I suspect)

Enrico Tassi (Oct 26 2021 at 08:05):

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.

Paolo Giarrusso (Oct 26 2021 at 08:13):

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.

• do we have a pattern match on e? Use destruct e — or destruct e eqn:Hname… but if we recurse on a piece, use induction instead. Often start top-down.

Paolo Giarrusso (Oct 26 2021 at 08:15):

Until now, we see:

• split does a pattern match and recursion on its input? We’ll need induction on it — and then simpl.
  Then we see that split does nested matches, on xy and on split l’: we _might_ need to use destruct on those.

Paolo Giarrusso (Oct 26 2021 at 08:17):

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).

Meven Lennon-Bertrand (Oct 26 2021 at 08:23):

Isn’t that more or less what functional induction does? Or the funelimtactic from Equations?

Paolo Giarrusso (Oct 26 2021 at 08:39):

indeed relevant, but I wouldn’t use either for Logical Foundations :wink: .

Meven Lennon-Bertrand (Oct 26 2021 at 08:49):

Sure! I only meant to say that this strategy has been at least automated, if not described ;)

drew (Oct 26 2021 at 12:07):

thanks everyone! will take another shot today.

drew (Oct 26 2021 at 14:45):

so, i've gotten this far:

drew (Oct 26 2021 at 14:46):

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.

drew (Oct 26 2021 at 14:46):

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'

drew (Oct 26 2021 at 14:46):

what i'm struggling with is that IHl' deals with the specific l' that i have from the induction

drew (Oct 26 2021 at 14:47):

if i add destruct xy as [x' y']. i get:

drew (Oct 26 2021 at 14:47):

match split l' with
| (lx, ly) => (x' :: lx, y' :: ly)
end = (l1, l2) -> combine l1 l2 = (x', y') :: l

as my goal

drew (Oct 26 2021 at 14:47):

which seems maybe closer?

Li-yao (Oct 26 2021 at 14:53):

It's alright that IHl' talks about l' because split l' is also in the goal.

Li-yao (Oct 26 2021 at 14:55):

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).

drew (Oct 26 2021 at 16:46):

oof, i got it, but i'm not sure it is ideal.

drew (Oct 26 2021 at 16:46):

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.

Paolo Giarrusso (Oct 26 2021 at 21:04):

you don’t need eqn:XY, but otherwise this looks reasonable.

Gaëtan Gilbert (Oct 26 2021 at 21:10):

hsplit doesn't look used either

Paolo Giarrusso (Oct 26 2021 at 21:12):

Ah! Doing simpl first avoids the need for it.

Paolo Giarrusso (Oct 26 2021 at 21:13):

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

drew (Oct 26 2021 at 22:36):

re the unused eqn lines, i’m following the author’s suggestion to always include them for now.

drew (Oct 26 2021 at 22:36):

once i understand the rules i will start breaking them :grinning:

drew (Nov 01 2021 at 13:48):

I'm working on this current sub-goal:

drew (Nov 01 2021 at 13:48):

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

drew (Nov 01 2021 at 13:48):

it looks to me like i should be able to rewrite <- IHl' but if i attempt to do so, I get:

drew (Nov 01 2021 at 13:48):

Unable to find an instance for the variable lf.

drew (Nov 01 2021 at 13:49):

this is confusing to me because IHl' seems that it should work for _all_ lf

drew (Nov 01 2021 at 13:49):

i guess maybe i have to intros H

drew (Nov 01 2021 at 14:06):

i'm also surprised i can't use discriminate on lf = x :: lf

drew (Nov 01 2021 at 14:09):

hey, i did it!

drew (Nov 01 2021 at 14:09):

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.

Kenji Maillard (Nov 01 2021 at 14:10):

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)

drew (Nov 01 2021 at 14:10):

@Kenji Maillard thanks. i was looking for an example of "applying" an generalized hypothesis. this helps.

drew (Nov 01 2021 at 14:11):

it turns out introducing lf earlier helped out here as well, which makes sense

Kenji Maillard (Nov 01 2021 at 14:21):

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)

Paolo Giarrusso (Nov 01 2021 at 21:56):

@Kenji Maillard True but confusing for many — non-experts would benefit from having a warning, or a variant of discriminate that would do the induction automatically on inductives…

Kenji Maillard (Nov 02 2021 at 08:37):

@Paolo Giarrusso I fully agree that discharging such goals easily would be something useful for non-experts, 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)...

Paolo Giarrusso (Nov 02 2021 at 08:43):

What about the “occurs check” from unification?

Paolo Giarrusso (Nov 02 2021 at 08:45):

sorry, you did say “strict subterm” :sweat_smile:

Paolo Giarrusso (Nov 02 2021 at 08:46):

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.

drew (Nov 03 2021 at 19:26):

i'm back! i'm working though the logic chapter and _close_ on this exercise:

drew (Nov 03 2021 at 19:26):

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.

drew (Nov 03 2021 at 19:27):

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')

drew (Nov 03 2021 at 19:28):

i've tried:

drew (Nov 03 2021 at 19:28):

right.
 apply IHl'.
 exists x.

drew (Nov 03 2021 at 19:28):

which gets me to:

drew (Nov 03 2021 at 19:28):

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'

drew (Nov 03 2021 at 19:29):

but i'm not sure how to deal with the fact that my H has a :: l' inside of it

drew (Nov 03 2021 at 19:30):

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 :|

drew (Nov 03 2021 at 19:32):

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.
      ++

Gaëtan Gilbert (Nov 03 2021 at 19:32):

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

drew (Nov 03 2021 at 19:32):

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'

drew (Nov 03 2021 at 19:32):

that's going further down the current path

Gaëtan Gilbert (Nov 03 2021 at 19:33):

go back to before you did right and do simpl in H

drew (Nov 03 2021 at 19:33):

AH, yes!

drew (Nov 03 2021 at 19:33):

that makes sense.

drew (Nov 03 2021 at 19:38):

phew!

drew (Nov 03 2021 at 19:38):

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.

drew (Nov 03 2021 at 19:38):

it feels like i overcomplicated this one

drew (Nov 03 2021 at 19:40):

is there a way to go to from H1 and H2 in context to H1 /\ H2 in context?

drew (Nov 03 2021 at 19:40):

that would simplify the last leg, at least

Gaëtan Gilbert (Nov 03 2021 at 19:49):

      destruct H as [H1 H2].
      destruct H2 as [H2 | H2].

you can combine this as destruct H as [H1 [H2 | H2]]

Gaëtan Gilbert (Nov 03 2021 at 19:49):

         split.
         +++ apply H1.
         +++ apply H2.

or split; assumption

Gaëtan Gilbert (Nov 03 2021 at 19:51):

or exact (conj H1 H2)

Gaëtan Gilbert (Nov 03 2021 at 19:52):

btw I see you go - + ++ +++ with bullets, but I think usually people use * after +

drew (Nov 03 2021 at 19:56):

thanks!

drew (Nov 03 2021 at 19:57):

but i'm not missing anything fundamental in these proofs so far? i appreciate all the feedback.

drew (Nov 04 2021 at 14:16):

i'm not sure where to go from here:

drew (Nov 04 2021 at 14:16):

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.

drew (Nov 04 2021 at 14:16):

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]

drew (Nov 04 2021 at 14:16):

unfolding rev_append doesn't seem to do much for me

Gaëtan Gilbert (Nov 04 2021 at 14:26):

you'll need to make some sort of lemma
consider how you would prove the theorem in a non formal way

drew (Nov 04 2021 at 14:48):

yes, i tried extracting a lemma saying exactly rev_append l' [x] = rev_append l' [ ] ++ [x]

drew (Nov 04 2021 at 14:49):

but then i struggled to solve that, for the same reason i'm struggling at this point :)

drew (Nov 04 2021 at 14:52):

basically i'm stuck here with a similar problem:

drew (Nov 04 2021 at 14:52):

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.
  -

drew (Nov 04 2021 at 14:53):

hmm wait, maybe i'm not!

drew (Nov 04 2021 at 15:00):

well i'm getting closer anyway

drew (Nov 04 2021 at 15:00):

 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.

drew (Nov 04 2021 at 15:02):

but i'm stuck in a sort of similar spot

drew (Nov 04 2021 at 15:02):

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

Gaëtan Gilbert (Nov 04 2021 at 15:04):

that's a weird lemma to try to prove

Gaëtan Gilbert (Nov 04 2021 at 15:05):

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)

Gaëtan Gilbert (Nov 04 2021 at 15:06):

(note you should be able to prove that goal, it's just not the nicest statement)

drew (Nov 04 2021 at 15:09):

hey i proved my gross lemma!

drew (Nov 04 2021 at 15:09):

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.

drew (Nov 04 2021 at 15:10):

i'll take a pass it at your lemma a bit later, thanks for the tips!

drew (Nov 05 2021 at 14:17):

ok i'm going bonkers with this "simple" 1 star exercise:

drew (Nov 05 2021 at 14:17):

Theorem eqb_neq : forall x y : nat,
  x =? y = false <-> x <> y.
Proof.
  intros x y.
  rewrite <- (not_true_is_false (x =? y)).

drew (Nov 05 2021 at 14:18):

2 subgoals

x, y : nat

========================= (1 / 2)

(x =? y) = (x =? y) <-> x <> y

========================= (2 / 2)

(x =? y) <> true

drew (Nov 05 2021 at 14:18):

i must be missing something fundamental because i don't see how to progress on these sub-goals

drew (Nov 05 2021 at 14:20):

one of my ideas was:

drew (Nov 05 2021 at 14:20):

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).

drew (Nov 05 2021 at 14:20):

but, uh,:

drew (Nov 05 2021 at 14:20):

2 subgoals
(1 unfocused at this level)

x, y : nat

========================= (1 / 2)

true = true -> x <> y

========================= (2 / 2)

false = false -> x <> y

Gaëtan Gilbert (Nov 05 2021 at 14:24):

the hint says not_true_iff_false(iff not is)

drew (Nov 05 2021 at 14:27):

well hey, that helps :)

drew (Nov 05 2021 at 14:37):

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.

drew (Nov 05 2021 at 14:37):

ok that did _not_ feel like one star

drew (Nov 05 2021 at 14:44):

i swear some of the 4 star exercises feel straight forward and some 1-2 star feel very challenging. perhaps it is related to my background in traditional pure FP that makes some exercises easier.

Quinn (Nov 05 2021 at 14:47):

i swear some of the 4 star exercises feel straight forward and some 1-2 star feel very challenging

we've all been there

drew (Nov 05 2021 at 14:47):

ha, thanks :)

Ana de Almeida Borges (Nov 05 2021 at 15:57):

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.

drew (Nov 05 2021 at 16:03):

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"

drew (Nov 05 2021 at 16:04):

so perhaps some things that are challenging for me would not be for folks going straight into phd programs

Ana de Almeida Borges (Nov 05 2021 at 16:24):

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.

Karl Palmskog (Nov 05 2021 at 16:31):

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

drew (Nov 05 2021 at 22:01):

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

drew (Nov 05 2021 at 22:02):

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"?

Gaëtan Gilbert (Nov 05 2021 at 22:02):

drew said:

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

injection H

Gaëtan Gilbert (Nov 05 2021 at 22:03):

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

drew (Nov 05 2021 at 22:04):

ah, that ; is sneaky, thanks!

drew (Nov 05 2021 at 22:05):

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?

drew (Nov 05 2021 at 22:06):

(thanks as always, very helpful)

Guillaume Melquiond (Nov 06 2021 at 05:30):

intros [= H1 H2]

Daniel Hilst Selli (Dec 02 2021 at 01:31):

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?

Li-yao (Dec 02 2021 at 01:54):

It's a lemma about rev_append you need, and since you defined it, you'll have to prove it.

Daniel Hilst Selli (Dec 02 2021 at 01:57):

Thanks @Li-yao I will try to write some auxiliary lemmas on rev_append

drew (Jan 06 2022 at 15:26):

hey all, i'm stuck on what seems like an obvious step in a proof.

drew (Jan 06 2022 at 15:26):

i'm here:

drew (Jan 06 2022 at 15:26):

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.

drew (Jan 06 2022 at 15:26):

with this following context:

drew (Jan 06 2022 at 15:26):

1 subgoal

m, n' : nat
En' : ev n'
IHn : ev m -> ev (n' + m)
Em : ev m

========================= (1 / 1)

ev (S (S (n' + m)))

drew (Jan 06 2022 at 15:27):

i have evSS_ev available to me, which seems like should "just work"

drew (Jan 06 2022 at 15:27):

but applying it _adds_ S (S .. rather than removing it

drew (Jan 06 2022 at 15:28):

am i on the wrong track? my other idea was to use induction on Em or use inversion.

drew (Jan 06 2022 at 15:30):

evSS_ev is:

drew (Jan 06 2022 at 15:30):

Theorem evSS_ev : forall n,
  ev (S (S n)) -> ev n.

Li-yao (Jan 06 2022 at 15:30):

You need a lemma with ev (S (S _)) as a conclusion.

Li-yao (Jan 06 2022 at 15:31):

Like ev_SS.

Li-yao (Jan 06 2022 at 15:31):

apply matches the conclusion of the lemma with the conclusion in your goal.

drew (Jan 06 2022 at 15:32):

wow, of course, i can use the constructor itself

drew (Jan 06 2022 at 15:32):

thanks, that's a facepalm moment

drew (Jan 06 2022 at 15:33):

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.

Gaëtan Gilbert (Jan 06 2022 at 15:46):

BTW here I would intro Em before doing the induction

drew (Jan 06 2022 at 15:48):

yes, good point

drew (Jan 06 2022 at 15:48):

i feel like i've gotten used to late intros when initially exploring a proof via induction

Gaëtan Gilbert (Jan 06 2022 at 16:51):

late intro would need to revert m here

Last updated: Sep 26 2023 at 13:01 UTC