Stream: Coq users

Topic: x = y -> S x = S y


view this post on Zulip Justin Kelm (Sep 04 2023 at 04:57):

I feel like I'm missing a simple tactic. How can I convert a goal of the form S x = S y into x = y for arbitrary expressions x, y and constructor S? What about f x = f y where f is not necessarily an invertible function? I know I can achieve it with rewrite if I need to, using enough or assert to get to that point, but I feel like there's a better way.

view this post on Zulip Guillaume Melquiond (Sep 04 2023 at 04:59):

apply f_equal (or just the f_equal tactic, for higher arity).

view this post on Zulip lilia Nejoua (Oct 31 2023 at 16:21):

can you help me how i can prouve that with succ_le_mono

view this post on Zulip lilia Nejoua (Oct 31 2023 at 16:21):

1987A872-1DF8-41A7-B988-8C86DBE86F08.png

view this post on Zulip Meven Lennon-Bertrand (Oct 31 2023 at 16:33):

@lilia Nejoua What is that? Also, to make it easier for us to help you, you should 1) post any new question in a new topic (go to the left, click ⋮ and "new topic"; 2) instead of screenshots, provide written code (enclosed in single backticks ` or triple backticks ```), so that people can copy-paste your code and experiment with it.

view this post on Zulip Théo Winterhalter (Oct 31 2023 at 16:35):

Also don't post the same question twice in two different topics.

view this post on Zulip Enrico Tassi (Nov 02 2023 at 12:08):

This looks like an assignent from some class..

view this post on Zulip Enrico Tassi (Nov 02 2023 at 12:09):

@Théo Zimmermann @Cyril Cohen

view this post on Zulip Pierre Rousselin (Nov 02 2023 at 12:39):

Yes, that's an assignment for my class (first year undergraduate). It's ok that the students ask questions here, I guess ("Beginner questions welcome"), and I gave them the link. It's true that this question was clumsily asked, but this is also something to learn.

view this post on Zulip Karl Palmskog (Nov 02 2023 at 12:47):

maybe good to ask your students to flag up that it's a homework question (so people know they ideally shouldn't solve everything completely, but rather give learning-friendly hints)

view this post on Zulip Karl Palmskog (Nov 02 2023 at 12:48):

indeed we would like to be welcoming to these kind of questions, but also help those that ask them with meta-problems like structuring the question.


Last updated: Jun 22 2024 at 15:01 UTC