[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

ADT axioms



> Resent-Date: Wed, 19 Nov 1997 09:19:30 -0800 (PST)
> Date: Wed, 19 Nov 1997 18:19:03 +0100
> From: Matteo Vaccari <vaccari@dsi.unimi.it>
> Organization: University of Milano Comp. Sci. Dept.
> Resent-From: pvs-help@csl.sri.com
> X-Mailing-List: <pvs-help@csl.sri.com> archive/latest/84
> X-Loop: pvs-help@csl.sri.com
> Precedence: list
> 
> Why is it that the extensionality axiom is an implication and not an
> equivalence?
> 
> I have a simple tree datatype:
> 
> tree[t:TYPE+] : DATATYPE
>   BEGIN
>     scalar (scalar: t): scalar?
>     pair   (left: tree, right: tree): pair?
>   END tree
> 
> among the automatically generated axioms I have
> 
>   tree_pair_extensionality: AXIOM
>         (FORALL (pair?_var: (pair?), pair?_var2: (pair?)):
>            left(pair?_var) = left(pair?_var2)
>                AND right(pair?_var) = right(pair?_var2)
>                IMPLIES pair?_var = pair?_var2);
> 
> but I'd like to be able to prove the reverse implication, for instance
> 
>   pair(a,b) = pair(c,d) IMPLIES a=c AND b=d
> 
> Am I missing something obvious?
> 
> Thank you in advance,
> 
> 	Matteo
> 
> 

I had the same problem with cons before pvs-help was set up.
Something along these lines should work (I haven't tested it).

(""
 (SKOSIMP*)
 (CASE "left(pair(a!1, b!1)) = left(pair(c!1, d!1))"
   "right(pair(a!1, b!1)) = right(pair(c!1, d!1))")
 (("1" (ASSERT)) ("2" (REPLACE*)) ("3" (REPLACE*))))

-- 
Paul Loewenstein          Sun Microsystems Inc., Mailstop UMPK12-302
Staff Engineer            901 San Antonio Road, Palo Alto, California 94303
		          Tel: 650-786-6015  FAX: 650-568-9603
                          paul.loewenstein@eng.sun.com