Implementing Sets with Lists

Implementing Sets with Lists
Associativity of union

We want to prove

S1,S2,S3:Set (S1 U (S2 U S3) = (S1 U S2) U S3) .

We use attribute coinduction to prove this is a behavorial property of the input specification.

First, we prove the attribute coherence of the input specification.

Introduce the lemma coherence(SET) .

This goal is true because coherence(SET) is in the hypothesis.

Then we prove S1,S2,S3:Set N:Nat N in S1 U (S2 U S3) = N in (S1 U S2) U S3

Quantifier elimination introduces new constants n :Nat and s1 s2 s3 :Set .

Show ( n in s1 U (s2 U s3) = n in (s1 U s2) U s3 ) by reduction.

Implementing Sets with Lists

The empty set is the unit of union.

We want to prove

S1:Set (empty U S1 = S1) .

We use attribute coinduction to prove this is a behavorial property of the input specification.

First, we prove the attribute coherence of the input specification.

Introduce the lemma coherence(SET) .

This goal is true because coherence(SET) is in the hypothesis.

Then we prove S1:Set (N:Nat ( N in empty U S1 = N in S1 ))

Quantifier elimination introduces new constants n :Nat and s1 :Set .

Show ( n in empty U s1 = n in s1 ) by reduction.

Implementing Sets with Lists

Idemopotency of union

We want to prove

S1:Set (S1 U S1 = S1) .

We use attribute coinduction to prove this is a behavorial property of the input specification.

First, we prove the attribute coherence of the input specification.

Introduce the lemma coherence(SET) .

This goal is true because coherence(SET) is in the hypothesis.

Then we prove S1:Set (N:Nat ( N in S1 U S1 = N in S1 ))

Quantifier elimination introduces new constants n :Nat and s1 :Set .

Show ( n in s1 U s1 = n in s1 ) by reduction.

Implementing Sets with Lists

Commutativity of union

We want to prove

S1,S2:Set (S1 U S2 = S2 U S1) .

We use attribute coinduction to prove this is a behavorial property of the input specification.

First, we prove the attribute coherence of the input specification.

Introduce the lemma coherence(SET) .

This goal is true because coherence(SET) is in the hypothesis.

Then we prove S1,S2:Set (N:Nat ( N in S1 U S2 = N in S2 U S1 ))

Quantifier elimination introduces new constants n :Nat and s1 s2 :Set .

Show ( n in s1 U s2 = n in s2 U s1 ) by reduction.

This page was generated by Kumo on Mon Jun 15 13:45:01 PDT 1998 from code written by Grigore Rosu,