Stream: Miscellaneous

Topic: ✔ chomp10s proof help


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: Jan 29 2023 at 18:03 UTC