Timeline for How can I prove this theorem with induction in Coq?
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 3, 2022 at 4:02 | answer | added | Malcolm Sharpe | timeline score: 2 | |
| Apr 23, 2022 at 12:40 | history | edited | Guy Coder |
edited tags
|
|
| Apr 23, 2022 at 11:51 | answer | added | pigworker | timeline score: 9 | |
| Apr 19, 2022 at 15:40 | vote | accept | Nova Sczerin | ||
| Apr 18, 2022 at 20:15 | answer | added | Couchy | timeline score: 2 | |
| Apr 18, 2022 at 17:23 | answer | added | Lessness Randomness | timeline score: 2 | |
| Apr 18, 2022 at 7:47 | comment | added | gallais | How would you prove it on paper? | |
| Apr 18, 2022 at 6:40 | comment | added | Nova Sczerin | is there a way to go about this without using the lia tactic? | |
| Apr 18, 2022 at 4:12 | comment | added | Couchy |
Also, the lia tactic (for linear arithmetic) is your best friend here, use Require Import Lia.
|
|
| Apr 18, 2022 at 2:06 | comment | added | Couchy |
You could try simpl (sum_n2 (S n)).
|
|
| Apr 18, 2022 at 1:53 | history | edited | Couchy | CC BY-SA 4.0 |
formatting
|
| Apr 18, 2022 at 1:09 | history | edited | Nova Sczerin | CC BY-SA 4.0 |
edited title
|
| S Apr 18, 2022 at 1:02 | review | First questions | |||
| Apr 18, 2022 at 4:24 | |||||
| S Apr 18, 2022 at 1:02 | history | asked | Nova Sczerin | CC BY-SA 4.0 |