Hey all, I have a minimal test case for what I'm trying to prove and getting stuck on. Any hints? https://gist.github.com/thomasdziedzic/3e59c6f787cdffc0b9e3554ba3c43395

Does the Theorem make sense? I'm trying to prove that chomp10s leaves a number that does not end with a 10 (binary). But I'm getting stuck at the induction step.

you need to do induction with 2 constructors at a step

one way to do that is to prove your statement also for `p`

minus one constructor:

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

alternatively you can use full power well founded induction

```
Require Import Wellfounded.Transitive_Closure Relation_Operators.
Inductive positive_size_lt : positive -> positive -> Prop :=
| xO_lt p : positive_size_lt p p~0
| xI_lt p : positive_size_lt p p~1.
Lemma wf_size_lt : well_founded positive_size_lt.
Proof.
intros p;induction p;constructor;intros p' H;inversion H;auto.
Qed.
Theorem chomp10s_correct : forall p : positive, ~ ends_with_10 (chomp10s p).
Proof.
apply (well_founded_induction (wf_clos_trans _ _ wf_size_lt)).
intros p IH Hp;destruct p;auto.
destruct p;auto.
apply IH with p;[|exact Hp].
do 3 econstructor.
Qed.
```

(auto does a lot of work there, you may want to remove it and manually prove the goals to see what's going on)

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

Thomas Dziedzic has marked this topic as resolved.

Hmm, I got the following error on the second branch in the first proof: `Tactic failure: tauto failed.`

specifically this line ` - split. 2:simpl;tauto.`

The 2nd proof using wellfounded works though, but I would still like to understand the first proof

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?

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)

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: Jun 10 2023 at 06:31 UTC