proposition: Theorem app_length : forall l1 l2 : natlist, length' (app' l1 l2) = ((length' l1) + (length' l2)).
proof: Proof. quickchick. Admitted. Theorem rev_app_distr: forall l1 l2 : natlist, rev' (app' l1 l2) = app' (rev' l2) (rev' l1). Proof. quickchick. Admitted. Theorem rev_involutive : forall l : natlist, rev' (rev' l) = l. Proof. quickchick. Admitted. Theorem rev_injective : forall (l1 l2 : natlist), rev' l1 = rev' l2 -> l1 = l2. Proof. quickchick. Admitted. Inductive ty : Type := | Ty_Bool : ty | Ty_Arrow : ty -> ty -> ty. Inductive tm : Type := | tm_var : string -> tm | tm_app : tm -> tm -> tm | tm_abs : string -> ty -> tm -> tm | tm_true : tm | tm_false : tm | tm_if : tm -> tm -> tm -> tm. Declare Custom Entry stlc. Notation "<{ e }>" := e (e custom stlc at level 99). Notation "( x )" := x (in custom stlc, x at level 99). Notation "x" := x (in custom stlc at level 0, x constr at level 0). Notation "S -> T" := (Ty_Arrow S T) (in custom stlc at level 50, right associativity). Notation "x y" := (tm_app x y) (in custom stlc at level 1, left associativity). Notation "\ x : t , y" := (tm_abs x t y) (in custom stlc at level 90, x at level 99, t custom stlc at level 99, y custom stlc at level 99, left associativity). Coercion tm_var : string >-> tm. Notation "'Bool'" := Ty_Bool (in custom stlc at level 0). Notation "'if' x 'then' y 'else' z" := (tm_if x y z) (in custom stlc at level 89, x custom stlc at level 99, y custom stlc at level 99, z custom stlc at level 99, left associativity). Notation "'true'" := true (at level 1). Notation "'true'" := tm_true (in custom stlc at level 0). Notation "'false'" := false (at level 1). Notation "'false'" := tm_false (in custom stlc at level 0). Definition x : string := "x". Definition y : string := "y". Definition z : string := "z". #[local] Hint Unfold x : core. #[local] Hint Unfold y : core. #[local] Hint Unfold z : core. Inductive value : tm -> Prop := | v_abs : forall x T2 t1, value <{\x:T2, t1}> | v_true : value <{true}> | v_false : value <{false}>. Inductive value_set : tm -> Set := | vs_abs : forall x T2 t1, value_set <{\x : T2, t1}> | vs_true : value_set <{true}> | vs_false : value_set <{false}> . Derive Show for ty. Derive Arbitrary for ty. Check elems_. #[export] Instance Gen_var : Gen string := {arbitrary := elems_ x (cons x (cons y (cons z nil)))}. #[export] Instance shrink_var : Shrink string := {shrink := fun s => match s with | "x"%string => cons y (cons z nil) | "y"%string => cons z nil | _ => nil end}. Derive Arbitrary for tm. Derive Show for tm. #[export] Instance Dec_eq_ty (T T' : ty) : Dec (T = T'). Proof. constructor. unfold ssrbool.decidable. decide equality. Defined.
imports: QuickChick(QuickChick) Coq(Nat) Coq(Arith.Arith) Coq(Logic.FunctionalExtensionality)