proof - Proving lemma with implication based on functions -

i want prove lemma below. trying to use tactic 'destruct', can't prove it. please body guide me how can prove such lemmas. can prove emptystring, not variables s1 , s2. thanks

inductive nat : set :=   | o : nat   | s : nat -> nat.    inductive string : set :=   | emptystring : string   | string : ascii -> string -> string.    fixpoint compstrings (sa : string) (sb : string) {struct sb}: bool :=   match sa   | emptystring => match sb                   | emptystring => true                   | string b sb'=> false                   end   | string sa' => match sb                    | emptystring => false                    | string b sb'=> compstrings sa' sb'                    end  end.   lemma eq_lenght : forall (s1 s2 : string),                   (compstrings s1 s2) = true -> (eq_nat (length s1) (length s2)) = true. 

first off, let me argue style. have written function compstrings this:

fixpoint compstrings' (sa : string) (sb : string) {struct sb}: bool :=   match sa, sb   | emptystring,  emptystring => true   | emptystring,  _   | _,            emptystring => false   | string sa', string b sb'=> compstrings sa' sb'   end. 

i find easier read. here proof it's same yours, in case you're suspicious:

theorem compstrings'ok: forall sa sb, compstrings sa sb = compstrings' sa sb. proof.   intros. destruct sa, sb; simpl; reflexivity. qed. 

---

now, two-fold answer. first i'm going hint @ direction proof. then, i'll give full proof encourage not read before you've tried yourself.

first off, assumed definition of length since did not provide it:

fixpoint length (s: string): nat :=   match s   | emptystring => o   | string _ rest => s (length rest)   end. 

and since did not have eq_nat either, proceeded prove lengths propositionally equal. should trivial adapt eq_nat.

lemma eq_length' : forall (s1 s2 : string),   compstrings s1 s2 = true ->   length s1 = length s2. proof.   induction s1.   (* todo *) admitted. 

so here start! want prove property inductive data type string. thing is, want proceed case analysis, if destructs, it'll never end. why proceed induction. is, need prove if s1 emptystring, property holds, , if property holds substring, holds string 1 character added. 2 cases simple, in each case can proceed case analysis on s2 (that is, using destruct).

note did not intros s1 s2 c. before doing induction s1.. important 1 reason: if (try!), induction hypothesis constrained talk 1 particular s2, rather being quantified it. can tricky when start doing proofs induction. so, sure try continue proof:

lemma eq_length'_will_fail : forall (s1 s2 : string),   compstrings s1 s2 = true ->   length s1 = length s2. proof.   intros s1 s2 c. induction s1.   (* todo *) admitted. 

eventually, you'll find induction hypothesis can't applied goal, because it's speaking particular s2.

---

i hope you've tried these 2 exercises.

now if you're stuck, here 1 way prove first goal.

don't cheat! :)

lemma eq_length' : forall (s1 s2 : string),   compstrings s1 s2 = true ->   length s1 = length s2. proof.   induction s1.   intros s2 c. destruct s2. reflexivity. inversion c.   intros s2 c. destruct s2. inversion c. simpl in *. f_equal.   exact (ihs1 _ c). qed. 

to put in intelligible terms:

• let's prove property forall s2, compstrings s1 s2 = true -> length s1 = s2 induction on s1:

  • in case s1 emptystring, let's @ shape of s2:

    1. s2 emptystring, both lengths equal 0, reflexivity.;

    2. s2 string _ _, there contradiction in hypothesis, shown inversion c.;

  • in case s1 string char1 rest1, let's @ shape of s2, supposing property true rest:

    1. s2 emptystring, there contradiction in hypothesis, show inversion c.;

    2. s2 string char2 rest2, length s1 = s (length rest1) , length s2 = s (length rest2), therefore need prove s (length rest1) = s (length rest2). also, hypothesis c simplifies c: compstrings rest1 rest2 = true. perfect occasion use induction hypothesis prove length rest1 = length rest2, , use result somehow prove goal.

note last step, there many ways proceed prove s (length rest1) = s (length rest2). 1 of using f_equal. asks prove pairwise equality between parameters of constructor. use rewrite (ihs1 _ c). use reflexivity on goal.

hopefully not solve particular goal, first understanding @ proofs induction!

---

to close on this, here 2 interesting links.

this presents basics of induction (see paragraph "induction on lists").

this explains, better me, why , how generalize induction hypotheses. you'll learn how solve goal did intros s1 s2 c. putting s2 in goal before starting induction, using tactic generalize (dependent).

in general, i'd recommend reading whole book. it's slow-paced , didactic.