[Práctica 5] Ejercicio 5

[Práctica 5] Ejercicio 5

de Cristian Fabian Sottile -
Número de respuestas: 1

Buenas tardes,

Escribo para consultar si hay alguna manera más compacta de hacer las pruebas de unicidad y corrección, ya que sobre todo la primera me quedó algo repetitiva en las partes inductivas.

Lemma unicidad : forall (e : BoolExpr) (m : Memoria) (w1 w2 : Valor),
  BEval e m w1 -> BEval e m w2 -> w1 = w2.
Proof.
  induction e; intros.
    inversion H; inversion H0; reflexivity.
    destruct b; inversion H; inversion H0; reflexivity.
    inversion_clear H; inversion_clear H0; auto.
      exact (IHe1 m false true H1 H).
      exact (IHe2 m false true H1 H2).
      exact (IHe1 m true false H1 H).
      exact (IHe2 m true false H2 H).
    inversion_clear H; inversion_clear H0; auto.
      exact (IHe m false true H H1).
      exact (IHe m true false H H1).
Qed.

Theorem correct_beval : forall (e : BoolExpr) (m : Memoria), BEval e m (beval m e).
Proof.
  intros e m; induction e; simpl.
    exact (evar v m).
    destruct b; [ exact (eboolt m) | exact (eboolf m) ].
    destruct (beval m e1); simpl.
      exact (andtrue e1 e2 m (beval m e2) IHe1 IHe2).
      exact (eandl e1 e2 m IHe1).
    destruct (beval m e0); simpl.
     exact (enott e0 m IHe).
     exact (enotf e0 m IHe).
Qed.
Gracias.
Saludos,
Cristian

                        

    
    
    
                            
    
    
                                

                                        
                                

    
                            
                    

                

            

        

    
        

                

                    

                        
                
                        

                            

                                        

                                                
                                        

                                

                                        En respuesta a Cristian Fabian Sottile
                                        
Re: [Práctica 5] Ejercicio 5

                                        

                                            de Carlos Luna - 
                        

                                

                            

                
                            

                                        

                                        

                
                                

                                    

                                        
Hola Cristian.
Se puede compactar un poco más usando compositores de tácticas y definiendo tácticas propias (algo que no vimos en el curso).
Para que la tácticas auto pueda aplicar algunos constructores de una definición inductiva I se puede poner, por ejemplo, Hint Constructors I. 
Sin usar nada de lo previo, igual se puede hacer una prueba más compacta, por ejemplo en la primer fijate algo como:
Proof.
  induction e; intros; auto.
    + inversion H. inversion H0. reflexivity.
    + destruct b; inversion H; inversion H0; reflexivity.
    + inversion H; inversion H0; auto.
    + inversion H; inversion H0; auto.
Qed. 
De todas maneras, no te preocupes. No esperamos que hagan pruebas minimalistas en este curso (se requieren algunos conceptos y herramientas adicionales, y un poco de experiencia, al menos).
Saludos, Carlos