Stream: Coq users

Topic: logical foundations


view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.
  -

view this post on Zulip drew (Oct 19 2021 at 13:51):

any hints?

view this post on Zulip 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

view this post on Zulip Alexander Gryzlov (Oct 19 2021 at 14:04):

Start with simpl again.

view this post on Zulip drew (Oct 19 2021 at 14:06):

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

view this post on Zulip 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

view this post on Zulip 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'.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 19 2021 at 14:11):

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

view this post on Zulip 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.

view this post on Zulip drew (Oct 19 2021 at 14:12):

thanks! these are very helpful tips. much appreciated!

view this post on Zulip drew (Oct 19 2021 at 14:13):

i've proven this earlier in the chapter:

view this post on Zulip 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.

view this post on Zulip drew (Oct 19 2021 at 14:13):

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

view this post on Zulip drew (Oct 19 2021 at 14:14):

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

view this post on Zulip 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.

view this post on Zulip drew (Oct 19 2021 at 14:17):

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

view this post on Zulip Notification Bot (Oct 19 2021 at 14:20):

Enrico Tassi has marked this topic as resolved.

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip 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

view this post on Zulip drew (Oct 21 2021 at 13:29):

but doing so causes an error:

view this post on Zulip drew (Oct 21 2021 at 13:30):

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

view this post on Zulip drew (Oct 21 2021 at 13:30):

am i totally on the wrong track?

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:30):

What about apply "eq_add_S in H"?

view this post on Zulip Gaëtan Gilbert (Oct 21 2021 at 13:30):

you want apply in not rewrite in

view this post on Zulip 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?

view this post on Zulip drew (Oct 21 2021 at 13:36):

phew, thanks to everyone!

view this post on Zulip 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.

view this post on Zulip drew (Oct 21 2021 at 13:36):

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

view this post on Zulip drew (Oct 21 2021 at 13:38):

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

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:38):

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

view this post on Zulip drew (Oct 21 2021 at 13:38):

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

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:39):

sorry, both infer them; no difference.

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:39):

but I might know what you mean.

view this post on Zulip 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

view this post on Zulip drew (Oct 21 2021 at 13:40):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:40):

with the same result.

view this post on Zulip 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

view this post on Zulip drew (Oct 21 2021 at 13:42):

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

view this post on Zulip drew (Oct 21 2021 at 13:42):

this is bidirectional implication?

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:42):

yes

view this post on Zulip drew (Oct 21 2021 at 13:42):

awesome, thanks for the thoughtful responses. very helpful!

view this post on Zulip 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.

view this post on Zulip drew (Oct 21 2021 at 13:42):

ah, hence the no m error

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:42):

which will fail because n could be anything!

view this post on Zulip 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

view this post on Zulip drew (Oct 21 2021 at 13:43):

lol

view this post on Zulip drew (Oct 21 2021 at 13:43):

i'm glad it's not just me

view this post on Zulip drew (Oct 21 2021 at 13:43):

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

view this post on Zulip drew (Oct 21 2021 at 13:44):

i think i get it!

view this post on Zulip drew (Oct 21 2021 at 13:44):

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

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:44):

yeah you’re doing good :-)

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:44):

and asking good questions

view this post on Zulip drew (Oct 21 2021 at 13:44):

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

view this post on Zulip 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)

view this post on Zulip drew (Oct 21 2021 at 13:45):

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

view this post on Zulip drew (Oct 21 2021 at 13:45):

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

view this post on Zulip drew (Oct 21 2021 at 13:45):

i'd be totally lost otherwise

view this post on Zulip 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

view this post on Zulip 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 ->?

view this post on Zulip drew (Oct 21 2021 at 13:47):

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

view this post on Zulip drew (Oct 21 2021 at 13:47):

sorry, totally ignores the left side, editing

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:47):

(deleted)

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Oct 21 2021 at 13:48):

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

view this post on Zulip 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

view this post on Zulip 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…

view this post on Zulip 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 .)

view this post on Zulip 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.

view this post on Zulip drew (Oct 21 2021 at 13:54):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 21 2021 at 14:04):

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

view this post on Zulip drew (Oct 21 2021 at 14:04):

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip drew (Oct 25 2021 at 14:09):

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

view this post on Zulip Notification Bot (Oct 25 2021 at 14:17):

Gaëtan Gilbert has marked this topic as unresolved.

view this post on Zulip 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?)

view this post on Zulip drew (Oct 25 2021 at 19:32):

i'm still struggling with this. current state:

view this post on Zulip 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.
  +

view this post on Zulip 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'

view this post on Zulip drew (Oct 25 2021 at 19:32):

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

view this post on Zulip drew (Oct 25 2021 at 19:33):

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

view this post on Zulip drew (Oct 25 2021 at 19:34):

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

view this post on Zulip drew (Oct 25 2021 at 19:34):

perhaps i need to do some destructing before my induction

view this post on Zulip Enrico Tassi (Oct 25 2021 at 19:39):

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

view this post on Zulip drew (Oct 25 2021 at 19:43):

i get to what feels like a similar spot:

view this post on Zulip 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'

view this post on Zulip drew (Oct 25 2021 at 19:59):

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

view this post on Zulip drew (Oct 25 2021 at 19:59):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 07:30):

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

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 07:40):

(but destruct will not come so late I suspect)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 08:15):

Until now, we see:

view this post on Zulip 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).

view this post on Zulip Meven Lennon-Bertrand (Oct 26 2021 at 08:23):

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

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 08:39):

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

view this post on Zulip 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 ;)

view this post on Zulip drew (Oct 26 2021 at 12:07):

thanks everyone! will take another shot today.

view this post on Zulip drew (Oct 26 2021 at 14:45):

so, i've gotten this far:

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip 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

view this post on Zulip drew (Oct 26 2021 at 14:47):

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

view this post on Zulip 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

view this post on Zulip drew (Oct 26 2021 at 14:47):

which seems maybe closer?

view this post on Zulip Li-yao (Oct 26 2021 at 14:53):

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

view this post on Zulip 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).

view this post on Zulip drew (Oct 26 2021 at 16:46):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 21:04):

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

view this post on Zulip Gaëtan Gilbert (Oct 26 2021 at 21:10):

hsplit doesn't look used either

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 21:12):

Ah! Doing simpl first avoids the need for it.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip drew (Oct 26 2021 at 22:36):

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

view this post on Zulip drew (Nov 01 2021 at 13:48):

I'm working on this current sub-goal:

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip drew (Nov 01 2021 at 13:48):

Unable to find an instance for the variable lf.

view this post on Zulip drew (Nov 01 2021 at 13:49):

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

view this post on Zulip drew (Nov 01 2021 at 13:49):

i guess maybe i have to intros H

view this post on Zulip drew (Nov 01 2021 at 14:06):

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

view this post on Zulip drew (Nov 01 2021 at 14:09):

hey, i did it!

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip drew (Nov 01 2021 at 14:10):

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

view this post on Zulip drew (Nov 01 2021 at 14:11):

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

view this post on Zulip 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)

view this post on Zulip 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…

view this post on Zulip 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)...

view this post on Zulip Paolo Giarrusso (Nov 02 2021 at 08:43):

What about the “occurs check” from unification?

view this post on Zulip Paolo Giarrusso (Nov 02 2021 at 08:45):

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

view this post on Zulip 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.

view this post on Zulip drew (Nov 03 2021 at 19:26):

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

view this post on Zulip 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.

view this post on Zulip 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')

view this post on Zulip drew (Nov 03 2021 at 19:28):

i've tried:

view this post on Zulip drew (Nov 03 2021 at 19:28):

right.
 apply IHl'.
 exists x.

view this post on Zulip drew (Nov 03 2021 at 19:28):

which gets me to:

view this post on Zulip 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'

view this post on Zulip 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

view this post on Zulip 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 :|

view this post on Zulip 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.
      ++

view this post on Zulip 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

view this post on Zulip 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'

view this post on Zulip drew (Nov 03 2021 at 19:32):

that's going further down the current path

view this post on Zulip Gaëtan Gilbert (Nov 03 2021 at 19:33):

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

view this post on Zulip drew (Nov 03 2021 at 19:33):

AH, yes!

view this post on Zulip drew (Nov 03 2021 at 19:33):

that makes sense.

view this post on Zulip drew (Nov 03 2021 at 19:38):

phew!

view this post on Zulip 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.

view this post on Zulip drew (Nov 03 2021 at 19:38):

it feels like i overcomplicated this one

view this post on Zulip 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?

view this post on Zulip drew (Nov 03 2021 at 19:40):

that would simplify the last leg, at least

view this post on Zulip 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]]

view this post on Zulip Gaëtan Gilbert (Nov 03 2021 at 19:49):

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

or split; assumption

view this post on Zulip Gaëtan Gilbert (Nov 03 2021 at 19:51):

or exact (conj H1 H2)

view this post on Zulip Gaëtan Gilbert (Nov 03 2021 at 19:52):

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

view this post on Zulip drew (Nov 03 2021 at 19:56):

thanks!

view this post on Zulip drew (Nov 03 2021 at 19:57):

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

view this post on Zulip drew (Nov 04 2021 at 14:16):

i'm not sure where to go from here:

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip drew (Nov 04 2021 at 14:16):

unfolding rev_append doesn't seem to do much for me

view this post on Zulip 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

view this post on Zulip drew (Nov 04 2021 at 14:48):

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

view this post on Zulip drew (Nov 04 2021 at 14:49):

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

view this post on Zulip drew (Nov 04 2021 at 14:52):

basically i'm stuck here with a similar problem:

view this post on Zulip 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.
  -

view this post on Zulip drew (Nov 04 2021 at 14:53):

hmm wait, maybe i'm not!

view this post on Zulip drew (Nov 04 2021 at 15:00):

well i'm getting closer anyway

view this post on Zulip 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.

view this post on Zulip drew (Nov 04 2021 at 15:02):

but i'm stuck in a sort of similar spot

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 04 2021 at 15:04):

that's a weird lemma to try to prove

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip drew (Nov 04 2021 at 15:09):

hey i proved my gross lemma!

view this post on Zulip 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.

view this post on Zulip drew (Nov 04 2021 at 15:10):

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

view this post on Zulip drew (Nov 05 2021 at 14:17):

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

view this post on Zulip 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)).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip drew (Nov 05 2021 at 14:20):

one of my ideas was:

view this post on Zulip 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).

view this post on Zulip drew (Nov 05 2021 at 14:20):

but, uh,:

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 05 2021 at 14:24):

the hint says not_true_iff_false(iff not is)

view this post on Zulip drew (Nov 05 2021 at 14:27):

well hey, that helps :)

view this post on Zulip 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.

view this post on Zulip drew (Nov 05 2021 at 14:37):

ok that did _not_ feel like one star

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip drew (Nov 05 2021 at 14:47):

ha, thanks :)

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip drew (Nov 05 2021 at 22:04):

ah, that ; is sneaky, thanks!

view this post on Zulip 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?

view this post on Zulip drew (Nov 05 2021 at 22:06):

(thanks as always, very helpful)

view this post on Zulip Guillaume Melquiond (Nov 06 2021 at 05:30):

intros [= H1 H2]

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Daniel Hilst Selli (Dec 02 2021 at 01:57):

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

view this post on Zulip drew (Jan 06 2022 at 15:26):

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

view this post on Zulip drew (Jan 06 2022 at 15:26):

i'm here:

view this post on Zulip 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.

view this post on Zulip drew (Jan 06 2022 at 15:26):

with this following context:

view this post on Zulip 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)))

view this post on Zulip drew (Jan 06 2022 at 15:27):

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

view this post on Zulip drew (Jan 06 2022 at 15:27):

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

view this post on Zulip 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.

view this post on Zulip drew (Jan 06 2022 at 15:30):

evSS_ev is:

view this post on Zulip drew (Jan 06 2022 at 15:30):

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

view this post on Zulip Li-yao (Jan 06 2022 at 15:30):

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

view this post on Zulip Li-yao (Jan 06 2022 at 15:31):

Like ev_SS.

view this post on Zulip Li-yao (Jan 06 2022 at 15:31):

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

view this post on Zulip drew (Jan 06 2022 at 15:32):

wow, of course, i can use the constructor itself

view this post on Zulip drew (Jan 06 2022 at 15:32):

thanks, that's a facepalm moment

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jan 06 2022 at 15:46):

BTW here I would intro Em before doing the induction

view this post on Zulip drew (Jan 06 2022 at 15:48):

yes, good point

view this post on Zulip drew (Jan 06 2022 at 15:48):

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

view this post on Zulip Gaëtan Gilbert (Jan 06 2022 at 16:51):

late intro would need to revert m here


Last updated: Feb 04 2023 at 22:29 UTC