CODEWITHSUNDEEP
coq
Sara
Sara

Reputation: 339

How to apply Fixpoint definitions within proofs in Coq?

I have some trouble understanding how to use some of the things I've defined in Coq within proofs. I have this fragment of definition and functions:

Inductive string : Set :=
| E  : string
| s  : nat -> string -> string.

Inductive deduce : Set :=
|de : string -> string -> deduce.

Infix "|=" := de. 

Inductive Rules : deduce -> Prop :=
| compress : forall (n   : nat) (A    : string), rule (( s n ( s n A))  |= ( s n A))
 | transitive : forall A B C : string, rule (A |= B) -> rule (B |= C) -> rule (A |= C).

Fixpoint RepString (n m : nat): string:=
match n with  
|0 => E
|S n => s m ( RepString n m)
end.

I need to prove something apparently easy but I bump into two problems:

Lemma LongCompress (C : string)(n : nat): n >=1 -> Rules 
((RepString n 0 ) |= (s 0 E) ).
Proof.
intros.
induction n.
inversion H.
simpl.
apply compress.

So here I have problem one, I get: 

"Unable to unify "Rules (s ?M1805 (s ?M1805 ?M1806) |= s ?M1805 ?M1806)" with 
"Rules (s 0 (RepString n 0) |- s 0 E)".'"

Now, I can see why I get the error, while technically RepString n 0 is the same as s 0 (s 0 (s 0( ... s 0 E))) I simply can't find the way to let coq know that, I've tried messing with apply compress with like 10 different things I still can't get it right. I need to "unfold" it something like that (of course unfold doesn't work...).

I'm out of ideas and I would very much appreciate any input you have on this!

EDIT FROM NOW ON.

Inductive Rules : deduce -> Prop :=
| compress : forall (n   : nat) (A    : string), rule (( s n ( s n A))  |= ( s n A))
 | transitive : forall A B C : string, rule (A |= B) -> rule (B |= C) -> rule (A |= C)
 | inspection : forall (n m : nat) (A    : string), m < n -> rule ((s n A) |- (s m A)).

 Definition less (n :nat )  (A B : string) :=  B |= (s n A).
 Lemma oneLess (n m : nat):  rule (less 0 (RepString n 1) (RepString m 1)) <-> n< m.

I have generalised the lemmas that Anton Trunov helped me prove, but now I bumped into another wall. I think the problem might start with the way I've written the Theorem itself, I will appreciate any ideas.

Upvotes: 3

Views: 1803

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15424

I'd prove something a little bit more general: for any two non-empty strings of zeros s = 0000...0 and t = 00...0, if length s > length t, then s |= t, i.e.

forall n m,
  m <> 0 ->
  n > m -> 
  Rules (RepString n 0 |= RepString m 0).

Here is a helper lemma:

Require Import Coq.Arith.Arith.
Require Import Coq.omega.Omega.
Hint Constructors Rules.  (* add this line after the definition of `Rules` *)

Lemma LongCompress_helper (n m k : nat):
  n = (S m) + k ->
  Rules (RepString (S n) 0 |= RepString (S m) 0).
Proof.
  generalize dependent m.
  generalize dependent n.
  induction k; intros n m H.
  - Search (?X + 0 = ?X). rewrite Nat.add_0_r in H.
    subst. simpl. eauto.
  - apply (transitive _ (RepString n 0) _); simpl in H; rewrite H.
    + simpl. constructor.
    + apply IHk. omega.
Qed.

Now, we can easily prove our advertised general lemma:

Lemma LongCompress_general (n m : nat):
  m <> 0 ->
  n > m -> 
  Rules (RepString n 0 |= RepString m 0).
Proof.
  intros Hm Hn. destruct n.
  - inversion Hn.
  - destruct m.
    + exfalso. now apply Hm.
    + apply LongCompress_helper with (k := n - m - 1). omega.
Qed.

It's easy to see that any sufficiently long string of zeros can be compressed into the singleton-string 0:

Lemma LongCompress (n : nat):
  n > 1 -> Rules ( RepString n 0  |= s 0 E ).
Proof.
  intro H. replace (s 0 E) with (RepString 1 0) by easy.
  apply LongCompress_general; auto.
Qed.

Upvotes: 6

Related Questions