From 413c2c75ee1c4e389efbaa35b30de886a28441c6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Mar 2008 12:40:49 +0000 Subject: [PATCH] letin are no longer unfolded thus coercions not propagated deeply. workaround not using letins --- .../matita/tests/coercions_russell.ma | 30 ++++++++----------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma index 203faece5..c386743e7 100644 --- a/helm/software/matita/tests/coercions_russell.ma +++ b/helm/software/matita/tests/coercions_russell.ma @@ -44,13 +44,13 @@ qed. alias symbol "exists" (instance 3) = "exists". lemma tl2 : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l. -letin program ≝ - (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]); -letin program_spec ≝ - (program : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l); - [ autobatch; | generalize in match H; clear H; cases s; simplify; - intros; cases (H H1); ] -exact program_spec. +apply + (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1] + : + ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l); +[ autobatch; +| generalize in match H; clear H; cases s; simplify; + intros; cases (H H1);] qed. definition nat_return := λn:nat. Some ? n. @@ -101,23 +101,19 @@ simplify; apply (eqb_elim x hd); simplify; intros; simplify; autobatch; qed. -definition if : ∀A:Type.bool → A → A → A ≝ - λA,b,t,f. match b with [ true ⇒ t | false ⇒ f]. - -notation < "'If' \nbsp b \nbsp 'Then' \nbsp t \nbsp 'Else' \nbsp f" for @{ 'if $b $t $f }. -notation > "'If' b 'Then' t 'Else' f" for @{ 'if $b $t $f }. -interpretation "if" 'if a b c = (cic:/matita/tests/coercions_russell/if.con _ a b c). +notation > "'If' b 'Then' t 'Else' f" +for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }. definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res). (* define the find function *) -letin find ≝ (λp. +apply (λp. let rec aux l ≝ match l with [ nil ⇒ raise_exn | cons x l ⇒ If p x Then nat_return x Else aux l] - in aux); -(* manca una delta?! *) unfold if in find; -apply (find: ∀p.∀l.sigma ? (λres.find_spec l p res)); clear find; + in aux + : + ∀p.∀l.sigma ? (λres.find_spec l p res)); (* l = x::tl ∧ p x = false *) [1: cases (aux l1); clear aux; generalize in match H2; clear H2; cases a; clear a; simplify; -- 2.39.2