From 4767d724d489a7ad67f696e9401e70b9f9ae2143 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 15 Oct 2007 19:55:12 +0000 Subject: Imported Upstream version 8.1.pl2+dfsg --- test-suite/success/cc.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index 42df990f..fecc8977 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -77,3 +77,22 @@ Theorem discr2 : Some true = Some false -> False. intros. congruence. Qed. + +Set Implicit Arguments. + +Parameter elt: Set. +Parameter elt_eq: forall (x y: elt), {x = y} + {x <> y}. +Definition t (A: Set) := elt -> A. +Definition get (A: Set) (x: elt) (m: t A) := m x. +Definition set (A: Set) (x: elt) (v: A) (m: t A) := + fun (y: elt) => if elt_eq y x then v else m y. +Lemma gsident: + forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m. +Proof. + intros. unfold get, set. case (elt_eq j i); intro. + congruence. + auto. +Qed. + + + \ No newline at end of file -- cgit v1.2.3