Thomas Dziedzic (Oct 16 2022 at 18:47): Thomas Dziedzic (Oct 16 2022 at 18:47):thanks for the tip @Gaëtan Gilbert I'll definitely work through this without auto since I don't understand something here and want to avoid any kind of magic for now :)
Notification Bot (Oct 16 2022 at 18:50):Thomas Dziedzic has marked this topic as resolved.
Thomas Dziedzic (Oct 16 2022 at 19:19):Hmm, I got the following error on the second branch in the first proof: Tactic failure: tauto failed.
Thomas Dziedzic (Oct 16 2022 at 19:19):specifically this line - split. 2:simpl;tauto.
Thomas Dziedzic (Oct 16 2022 at 19:25):The 2nd proof using wellfounded works though, but I would still like to understand the first proof
Gaëtan Gilbert (Oct 16 2022 at 19:32):with full script
Require Import Coq.PArith.BinPos.
Require Import Coq.NArith.BinNat.
Open Scope positive_scope.
Open Scope N_scope.
Fixpoint chomp10s (p : positive) : N :=
match p with
| p'~1~0 => chomp10s p'
| 1~0 => N0
| _ => Npos p
end.
Definition ends_with_10 (n : N) : Prop :=
match n with
| N0 => False
| Npos p =>
match p with
| p'~1~0 => True
| 1~0 => True
| _ => False
end
end.
Definition pseudopred p :=
match p with
| p~1 | p~0 => p
| xH => xH
end.
Theorem chomp10s_correct : forall p : positive, ~ ends_with_10 (chomp10s p) /\ ~ ends_with_10 (chomp10s (pseudopred p)).
Proof.
unfold not.
induction p.
- simpl. tauto.
- split. 2:simpl;tauto.
destruct p;simpl in *;tauto.
- simpl;tauto.
Qed.
?
what coq version?
Gaëtan Gilbert (Oct 16 2022 at 19:33):what about
Theorem chomp10s_correct : forall p : positive, ~ ends_with_10 (chomp10s p) /\ ~ ends_with_10 (chomp10s (pseudopred p)).
Proof.
unfold not.
induction p.
- simpl. tauto.
- split.
+ destruct p;simpl in *;tauto.
+ destruct IHp as [IHp _];exact IHp.
- simpl;tauto.
Qed.
for the proof? (this is what 2:simpl;tauto does)
Thomas Dziedzic (Oct 16 2022 at 19:37):I spotted my mistake, I didn't copy and paste the pseudopred function and it was wrong. Now your proof works for me! thanks!
Last updated: Jan 29 2023 at 18:03 UTC