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)


Last updated: Jan 29 2023 at 18:03 UTC