Stream: Miscellaneous

Topic: ✔ chomp10s proof help


view this post on Zulip Thomas Dziedzic (Oct 16 2022 at 16:20):

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.

view this post on Zulip Gaëtan Gilbert (Oct 16 2022 at 16:54):

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)

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

view this post on Zulip Notification Bot (Oct 16 2022 at 18:50):

Thomas Dziedzic has marked this topic as resolved.

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

view this post on Zulip Thomas Dziedzic (Oct 16 2022 at 19:19):

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

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

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

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

view this post on Zulip 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: Mar 28 2024 at 17:01 UTC