From: Claudio Sacerdoti Coen Date: Mon, 5 Sep 2005 16:59:40 +0000 (+0000) Subject: ... X-Git-Tag: V_0_1_2_1~90 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0c2b65693a5a7a2881ebb6dfcaa432f4f9fd22a4;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 7f5cb644f..c29a9a031 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -14,7 +14,19 @@ TODO - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire, giusto? - comportamento di tutte le tattiche nei confronti dei let-in - - tattica unfold su rel a let-in bound variables + - tattica unfold su rel a let-in bound variables: c'e' ancora un bug + aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto + del goal e non in quello del pattern. Pertanto invece di cercare di + fare unfolding di x viene fatto unfolding di altro. + Soluzione: la funzione ProofEngineHelpers.select deve tornare una + funzione per rilocare i termini nel contesto giusto. + Esempio: + theorem t: let uno \def S O in uno + uno = S uno \to uno=uno. + intros. unfold uno in H. + NOTA: questo bug e' legato a quello di parsing in presenza di tattiche + con pattern, visto che in tal caso e' l'intero parsing a dover essere + fatto in un contesto differente. Risolvendo quel bug si risolve + automaticamente anche questo. - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con True. - parsing contestuale (tattiche replace, change e forse altre) diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma index 28ffcf3f2..4af22f1b9 100644 --- a/helm/matita/tests/unfold.ma +++ b/helm/matita/tests/unfold.ma @@ -30,3 +30,8 @@ theorem trivial: \forall n. S (myplus n n) = myplus (S n) n. rewrite > lem. reflexivity. qed. + +(* This test needs to parse "uno" in the context of the hypothesis H, + not in the context of the goal. *) +theorem t: let uno \def S O in uno + uno = S uno \to uno=uno. + intros. unfold uno in H.